Matt Kaufmann
- Mechanized reasoning
- 2005 ACM Software System Award
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.
Co-author, ACL2 Theorem Prover (http://www.cs.utexas.edu/users/moore/acl2/).
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)
