Matt Kaufmann

Matt Kaufmann, J. Strother Moore: Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1. ACL2 2013: 5-12

Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann: Abstract Stobjs and Their Application to ISA Modeling. ACL2 2013: 54-69

Warren A. Hunt Jr., Matt Kaufmann: A formal model of a large memory that supports efficient execution. FMCAD 2012: 60-67

Michael J. C. Gordon, Matt Kaufmann, Sandip Ray: The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. J. Autom. Reasoning 47(1): 1-16 (2011)

Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios: Integrating Testing and Interactive Theorem Proving. ACL2 2011: 4-19

Matt Kaufmann, J. Strother Moore: How Can I Do That with ACL2? Recent Enhancements to ACL2. ACL2 2011: 46-60

Matt Kaufmann, Lawrence C. Paulson (Eds.): Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science 6172, Springer 2010, isbn 978-3-642-14051-8

Matt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber: Integrating external deduction tools with ACL2. J. Applied Logic 7(1): 3-25 (2009)

Bishop Brock, Matt Kaufmann, J. Strother Moore: Rewriting with Equivalence Relations in ACL2. J. Autom. Reasoning 40(4): 293-306 (2008)

David A. Greve, Matt Kaufmann, Panagiotis Manolios, J. Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1): 15-46 (2008)

Matt Kaufmann, J. Strother Moore: An ACL2 Tutorial. TPHOLs 2008: 17-21

Matt Kaufmann, Konrad Slind: Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon ₀. TPHOLs 2007: 294-301

Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds: An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46

Matt Kaufmann, J. Strother Moore: Double rewriting for equivalential reasoning in ACL2. ACL2 2006: 103-106

Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann: An Integration of HOL and ACL2. FMCAD 2006: 153-160

Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith: Meta Reasoning in ACL2. TPHOLs 2005: 163-178

Matt Kaufmann, J. Strother Moore: Structured Theory Development for a Mechanized Logic. J. Autom. Reasoning 26(2): 161-203 (2001)

Ruben Gamboa, Matt Kaufmann: Nonstandard Analysis in ACL2. J. Autom. Reasoning 27(4): 323-351 (2001)

Matt Kaufmann: Verification of Year 2000 conversion rules using the ACL2 theorem prover. STTT 3(1): 13-19 (2000)

J. Strother Moore, Thomas W. Lynch, Matt Kaufmann: A Mechanically Checked Proof of the AMD5_K86^TM Floating Point Division Program. IEEE Trans. Computers 47(9): 913-926 (1998)

Matt Kaufmann: ACL2 Support for Verification Projects (Invited Talk). CADE 1998: 220-238

Matt Kaufmann, Andrew Martin, Carl Pixley: Design Constraints in Symbolic Model Checking. CAV 1998: 477-487

Matt Kaufmann, J. Strother Moore: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. 23(4): 203-213 (1997)

Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley: Formal Verification of FIRE: A Case Study. DAC 1997: 173-177

Matt Kaufmann, Carl Pixley: Intertwined Development and Formal Verification of a 60x Bus Model. ICCD 1997: 25-30

Matt Kaufmann, Paolo Pecchiari: Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. J. Autom. Reasoning 16(1-2): 181-222 (1996)

Bishop Brock, Matt Kaufmann, J. Strother Moore: ACL2 Theorems About Commercial Microprocessors. FMCAD 1996: 275-293

Carl Pixley, Noel R. Strader, W. C. Bruce, Jaehong Park, Matt Kaufmann, Kurt Shultz, Michael Burns, Jainendra Kumar, Jun Yuan, Janet Nguyen: Commercial Design Verification: Methodology and Tools. ITC 1996: 839-848

Matt Kaufmann: An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. J. Autom. Reasoning 9(3): 355-372 (1992)

Matt Kaufmann: Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm. J. Autom. Reasoning 7(1): 109-158 (1991)

Matt Kaufmann: An Informal Discussion of Issues in Mechanically-Assisted Reasoning. TPHOLs 1991: 318-337

Matt Kaufmann: RCL: A Lisp Verification System. CADE 1990: 659-660

Matt Kaufmann: An Interactive Enhancement to the Boyer-Moore Theorem Prover. CADE 1988: 735-736

Matt Kaufmann, James H. Schmerl: Remarks on Weak Notions of Saturation in Models of Peano Arithmetic. J. Symb. Log. 52(1): 129-148 (1987)

Matt Kaufmann, Saharon Shelah: On random models of finite power and monadic logic. Discrete Mathematics 54(3): 285-293 (1985)

John T. Baldwin, Matt Kaufmann, Julia F. Knight: Meeting of the Association for Symbolic Logic: Notre Dame, Indiana, 1984. J. Symb. Log. 50(1): 284-286 (1985)

Matt Kaufmann: Filter Logics on omega. J. Symb. Log. 49(1): 241-256 (1984)

C. Ward Henson, Matt Kaufmann, H. Jerome Keisler: The Strength of Nonstandard Methods in Arithmetic. J. Symb. Log. 49(4): 1039-1058 (1984)

Matt Kaufmann: Set Theory With a Filter Quantifier. J. Symb. Log. 48(2): 263-287 (1983)

Matt Kaufmann: Blunt and Topless End Extensions of Models of Set Theory. J. Symb. Log. 48(4): 1053-1073 (1983)

Matt Kaufmann: A New Omitting Types Theorem for L(Q). J. Symb. Log. 44(4): 507-521 (1979)