Matt Kaufmann

Publication Activity (10 Years)

Years Active: 1979-2023
Publications (10 Years): 14

Top Topics

Natural Language Learning

Formal Verification

Top Venues

Arch. Math. Log.

Publications

Matt Kaufmann, J Strother Moore
Advances in ACL2 Proof Debugging Tools. CoRR (2023)
Matt Kaufmann, J. Strother Moore
Iteration in ACL2. ACL2 (2020)
Matt Kaufmann, J. Strother Moore
Limited Second-Order Functionality in a First-Order Setting. J. Autom. Reason. 64 (3) (2020)
Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland
A Hierarchical Approach to Self-Timed Circuit Verification. ASYNC (2019)
Ali Enayat, Matt Kaufmann, Zachiri McKenzie
Largest initial segments pointwise fixed by automorphisms of models of set theory. Arch. Math. Log. 57 (1-2) (2018)
Ali Enayat, Matt Kaufmann, Zachiri McKenzie
Iterated ultrapowers for the masses. Arch. Math. Log. 57 (5-6) (2018)
Matt Kaufmann
DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract). ACL2 (2018)
Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland
Data-Loop-Free Self-Timed Circuit Verification. ASYNC (2018)
Matt Kaufmann, Sol Swords
Meta-extract: Using Existing Facts in Meta-reasoning. ACL2 (2017)
Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler
Efficient, Verified Checking of Propositional Proofs. ITP (2017)
Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith
A Versatile, Sound Tool for Simplifying Definitions. ACL2 (2017)
Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
Efficient Certified RAT Verification. CADE (2017)
Luís Cruz-Filipe, Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
Efficient Certified RAT Verification. CoRR (2016)
Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.
Fourier Series Formalization in ACL2(r). ACL2 (2015)
Matt Kaufmann, J Strother Moore
Rough Diamond: An Extension of Equivalence-Based Rewriting. ITP (2014)
Matt Kaufmann, J Strother Moore
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. ACL2 (2014)
Jared Davis, Matt Kaufmann
Industrial-Strength Documentation for ACL2. ACL2 (2014)
Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh
Simulation and formal verification of x86 machine-code programs that make system calls. FMCAD (2014)
Matt Kaufmann, J Strother Moore
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 ACL2 (2013)
David L. Rager, Warren A. Hunt Jr., Matt Kaufmann
A Parallelized Theorem Prover for a Logic with Parallel Execution. ITP (2013)
Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann
Abstract Stobjs and Their Application to ISA Modeling ACL2 (2013)
Warren A. Hunt Jr., Matt Kaufmann
A formal model of a large memory that supports efficient execution. FMCAD (2012)
David L. Rager, Warren A. Hunt Jr., Matt Kaufmann
A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp. ELS (2011)
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. Reason. 47 (1) (2011)
Matt Kaufmann, J Strother Moore
How Can I Do That with ACL2? Recent Enhancements to ACL2 ACL2 (2011)
Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios
Integrating Testing and Interactive Theorem Proving ACL2 (2011)
Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber
Integrating external deduction tools with ACL2. J. Appl. Log. 7 (1) (2009)
Matt Kaufmann, J Strother Moore
An ACL2 Tutorial. TPHOLs (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) (2008)
Bishop Brock, Matt Kaufmann, J Strother Moore
Rewriting with Equivalence Relations in ACL2. J. Autom. Reason. 40 (4) (2008)
Matt Kaufmann, Konrad Slind
. TPHOLs (2007)
Matt Kaufmann, J Strother Moore
Double rewriting for equivalential reasoning in ACL2. ACL2 (2006)
Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds
An embedding of the ACL2 logic in HOL. ACL2 (2006)
Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
An Integration of HOL and ACL2. FMCAD (2006)
Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
Meta Reasoning in ACL2. TPHOLs (2005)
Matt Kaufmann, J Strother Moore
Structured Theory Development for a Mechanized Logic. J. Autom. Reason. 26 (2) (2001)
Ruben Gamboa, Matt Kaufmann
Nonstandard Analysis in ACL2. J. Autom. Reason. 27 (4) (2001)
Matt Kaufmann
Verification of Year 2000 conversion rules using the ACL2 theorem prover. Int. J. Softw. Tools Technol. Transf. 3 (1) (2000)
Matt Kaufmann, Andrew Martin, Carl Pixley
Design Constraints in Symbolic Model Checking. CAV (1998)
J. Strother Moore, Thomas W. Lynch, Matt Kaufmann
Floating Point Division Program. IEEE Trans. Computers 47 (9) (1998)
Matt Kaufmann
ACL2 Support for Verification Projects (Invited Talk). CADE (1998)
Matt Kaufmann, J. Strother Moore
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. 23 (4) (1997)
Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley
Formal Verification of FIRE: A Case Study. DAC (1997)
Matt Kaufmann, Carl Pixley
Intertwined Development and Formal Verification of a 60x Bus Model. ICCD (1997)
Matt Kaufmann, Paolo Pecchiari
Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. J. Autom. Reason. 16 (1-2) (1996)
Bishop Brock, Matt Kaufmann, J. Strother Moore
ACL2 Theorems About Commercial Microprocessors. FMCAD (1996)
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)
Matt Kaufmann
An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. J. Autom. Reason. 9 (3) (1992)
Matt Kaufmann
An Informal Discussion of Issues in Mechanically-Assisted Reasoning. TPHOLs (1991)
Matt Kaufmann
Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm. J. Autom. Reason. 7 (1) (1991)
Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J. Strother Moore
Functional Instantiation in First-Order Logic. Artificial and Mathematical Theory of Computation (1991)
Matt Kaufmann
RCL: A Lisp Verification System. CADE (1990)
Matt Kaufmann
An Interactive Enhancement to the Boyer-Moore Theorem Prover. CADE (1988)
Matt Kaufmann, James H. Schmerl
Remarks on Weak Notions of Saturation in Models of Peano Arithmetic. J. Symb. Log. 52 (1) (1987)
Matt Kaufmann, Saharon Shelah
The Hanf number of stationary logic. Notre Dame J. Formal Log. 27 (1) (1986)
Robert S. Boyer, Matt Kaufmann
A prototype theorem-prover for a higher-order functional language. ACM SIGSOFT Softw. Eng. Notes 10 (4) (1985)
Matt Kaufmann, Saharon Shelah
On random models of finite power and monadic logic. Discret. Math. 54 (3) (1985)
Matt Kaufmann
A note on the Hanf number of second-order logic. Notre Dame J. Formal Log. 26 (4) (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) (1985)
Matt Kaufmann, James H. Schmerl
Saturation and simple extensions of models of peano arithmetic. Ann. Pure Appl. Log. 27 (2) (1984)
Matt Kaufmann, Saharon Shelah
A nonconservativity result on global choice. Ann. Pure Appl. Log. 27 (3) (1984)
Matt Kaufmann
Filter Logics on omega. J. Symb. Log. 49 (1) (1984)
Matt Kaufmann, Evangelos Kranakis
Definable Ultrapowers and Ultrafilters over Admissible Ordinals. Math. Log. Q. 30 (7-8) (1984)
Matt Kaufmann
Some remarks on equivalence in infinitary and stationary logic. Notre Dame J. Formal Log. 25 (4) (1984)
C. Ward Henson, Matt Kaufmann, H. Jerome Keisler
The Strength of Nonstandard Methods in Arithmetic. J. Symb. Log. 49 (4) (1984)
Matt Kaufmann
Set Theory With a Filter Quantifier. J. Symb. Log. 48 (2) (1983)
Matt Kaufmann
Blunt and Topless End Extensions of Models of Set Theory. J. Symb. Log. 48 (4) (1983)
Matt Kaufmann
A New Omitting Types Theorem for L(Q). J. Symb. Log. 44 (4) (1979)