Matt Kaufmann

Senior Research Scientist
GDC 7.804
(512) 471-9780
kaufmann [at] cs [dot] utexas [dot] edu
  • Mechanized reasoning
UTCS Research Areas: 
Selected Awards & Honors: 
  • 2005 ACM Software System Award
Selected Publications: 

Integrating External Deduction Tools with ACL2 (with J S. Moore,
Sandip Ray, and Erik Reeber). Journal of Applied Logic
(Special Issue: Empirically Successful Computerized Reasoning),
Volume 7, Issue 1, March 2009, pp. 3--25.  Also published online
(DOI 10.1016/j.jal.2007.07.002).

Efficient Execution in an Automated Reasoning Environment (with
David A. Greve, Panagiotis Manolios, J Strother Moore, Sandip Ray,
Jose Luis Ruiz-Reina, Rob Sumners, Daron Vroon, and Matthew
Wilding).  Journal of Functional Programming, Volume 18, Issue 01,
January 2008, Cambridge University Press.

Structured Theory Development for a Mechanized Logic (with J Moore).
Journal of Automated Reasoning 26, no. 2 (2001) 161-203.

A Mechanically Checked Proof of the AMD5 Floating-Point
Division Program (with J Moore and T. Lynch). IEEE
Trans. Computers 47, no. 9 (1998), pp. 913--926.

Stationary Logic (with J. Barwise and M. Makkai).
Ann. Math. Logic 13 (1978), pp. 171-224.

  • "Computer-Aided Reasoning: An Approach" (with P. Manolios and J Moore).  Kluwer Academic Publishers, June, 2000.
  • "Computer-Aided Reasoning: ACL2 Case Studies" (with co-editors P. Manolios and J Moore).  Kluwer Academic Publishers, June, 2000.
  • (Chapter) ACL2 and Its Applications to Digital System Verification (with J Strother Moore).  In: "Design and Verification of Microprocessor Systems for High-Assurance Applications", David S.~Hardin, ed., Springer, 2010, pp. 1--21.
  • (Chapter) A Computational Logic for Applicative Common Lisp (with J Moore).  In: "A Companion to Philosophical Logic", D. Jacquette (ed), Blackwell Publishers, pp. 724-741, 2002.
  • (Chapter) The Quantifier "There Exist Uncountably Many" and Some of Its Relatives, in: Model-Theoretic Logics (J. Barwise and S. Feferman, editors), Springer-Verlag, 1985, pp. 123-176.
Professional Activities: 

Co-author, ACL2 Theorem Prover (

The usual academic activities (service on program committees and other paper reviewing; service on Ph.D. committees)

In particular, served as conference co-chair, International Conference on Interactive Theorem Proving, Edinburgh, Scotland, July 2010 (ITP 2010)