Computer Science

Ruben Gamboa

Education

• 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

Professional Experience

• Professor, University of Wyoming, 2015-present
• Associate Professor, University of Wyoming, 2007-2015
• 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

Research Interests
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.

Visit Dr. Gamboa's website for more information!