- M.S. (Astronomy) Swinburne Technical University (Online), 2013
- Ph.D. University of Texas at Austin 1999
- M.C.S. Texas A&M University 1986
- B.S. Angelo State University 1984
- Associate Professor, University of Wyoming, 2007-present
- Assistant Professor, University of Wyoming, 2002-2007
- Member, Technical Advisory Group, Morningstar, 2010-2011
- Member, Technical Advisory Board, Logical Information Machines (LIM), 2000-2010
- V.P. of Engineering, Loop One, 2000-2001
- Founder and Member of Board of Directors, Logical Information Machines (LIM), 1990-2000
- Junior Member, Technical Staff, Microelectronics and Computer Technology Corporation (MCC), 1988-1989
ACL2, formalization of mathematics, automated theorem proving, applications of cloud computing and NoSQL databases
Current Research Projects
- Continuing the ACL2(r) formalization of the transcendental functions in the x86 instruction set. This project is motivated by work of David Russinoff originally at AMD and now at Intel.
- Continuing the formalization of various sequences and series in ACL2(r). Of particular interest are the convergence and divergence of summations of reciprocals of various sets of numbers, e.g., primes.
- Proving Lindemann’s theorem and the transcendence of e and π in ACL2(r). This project is in support of a practical verification effort at Intel.
- Exploring the formalization of analog circuits in ACL2(r). This project is of interest to engineers at Centaur Technology, who use formal methods to reason about digital designs and would like a similar support for analog design.