Matt Kaufmann

According to our database, Matt Kaufmann authored at least 69 papers between 1979 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of two.

2023

Advances in ACL2 Proof Debugging Tools.

Matt Kaufmann, J Strother Moore

Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, 2023

2020

Limited Second-Order Functionality in a First-Order Setting.

Matt Kaufmann, J Strother Moore

J. Autom. Reason., 2020

Iteration in ACL2.

Matt Kaufmann, J Strother Moore

Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, 2020

2019

A Hierarchical Approach to Self-Timed Circuit Verification.

Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland

Proceedings of the 25th IEEE International Symposium on Asynchronous Circuits and Systems, 2019

2018

DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract).

Matt Kaufmann

Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, 2018

Iterated ultrapowers for the masses.

Ali Enayat, Matt Kaufmann, Zachiri McKenzie

Arch. Math. Log., 2018

Largest initial segments pointwise fixed by automorphisms of models of set theory.

Ali Enayat, Matt Kaufmann, Zachiri McKenzie

Arch. Math. Log., 2018

Data-Loop-Free Self-Timed Circuit Verification.

Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland

Proceedings of the 24th IEEE International Symposium on Asynchronous Circuits and Systems, 2018

2017

Meta-extract: Using Existing Facts in Meta-reasoning.

Matt Kaufmann, Sol Swords

Proceedings of the Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, 2017

A Versatile, Sound Tool for Simplifying Definitions.

Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith

Proceedings of the Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, 2017

Efficient, Verified Checking of Propositional Proofs.

Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Efficient Certified RAT Verification.

Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp

Proceedings of the Automated Deduction - CADE 26, 2017

Engineering a Formal, Executable x86 ISA Simulator for Software Verification.

Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann

Proceedings of the Provably Correct Systems, 2017

2015

Fourier Series Formalization in ACL2(r).

Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.

Proceedings of the Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, 2015

2014

Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4.

Matt Kaufmann, J Strother Moore

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Industrial-Strength Documentation for ACL2.

Jared Davis, Matt Kaufmann

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Rough Diamond: An Extension of Equivalence-Based Rewriting.

Matt Kaufmann, J Strother Moore

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Simulation and formal verification of x86 machine-code programs that make system calls.

Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh

Proceedings of the Formal Methods in Computer-Aided Design, 2014

2013

Abstract Stobjs and Their Application to ISA Modeling

Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1

Matt Kaufmann, J Strother Moore

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

A Parallelized Theorem Prover for a Logic with Parallel Execution.

David L. Rager, Warren A. Hunt Jr., Matt Kaufmann

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

A formal model of a large memory that supports efficient execution.

Warren A. Hunt Jr., Matt Kaufmann

Proceedings of the Formal Methods in Computer-Aided Design, 2012

2011

The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4.

Michael J. C. Gordon, Matt Kaufmann, Sandip Ray

J. Autom. Reason., 2011

How Can I Do That with ACL2? Recent Enhancements to ACL2

Matt Kaufmann, J Strother Moore

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

Integrating Testing and Interactive Theorem Proving

Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp.

David L. Rager, Warren A. Hunt Jr., Matt Kaufmann

Proceedings of ELS 2011 - 4th European Lisp Symposium, Hamburg, Germany, March 31, 2011

2010

ACL2 and Its Applications to Digital System Verification.

Matt Kaufmann, J Strother Moore

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Integrating external deduction tools with ACL2.

Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber

J. Appl. Log., 2009

2008

Efficient execution in an automated reasoning environment.

David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding

J. Funct. Program., 2008

Rewriting with Equivalence Relations in ACL2.

Bishop Brock, Matt Kaufmann, J Strother Moore

J. Autom. Reason., 2008

An ACL2 Tutorial.

Matt Kaufmann, J Strother Moore

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

2007

Proof Pearl: Wellfounded Induction on the Ordinals Up to <i>epsilon</i> ₀.

Matt Kaufmann, Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

2006

An Integration of HOL and ACL2.

Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

Double rewriting for equivalential reasoning in ACL2.

Matt Kaufmann, J Strother Moore

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

An embedding of the ACL2 logic in HOL.

Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2005

Meta Reasoning in ACL2.

Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

2001

Structured Theory Development for a Mechanized Logic.

Matt Kaufmann, J Strother Moore

J. Autom. Reason., 2001

Nonstandard Analysis in ACL2.

Ruben Gamboa, Matt Kaufmann

J. Autom. Reason., 2001

2000

Verification of Year 2000 conversion rules using the ACL2 theorem prover.

Matt Kaufmann

Int. J. Softw. Tools Technol. Transf., 2000

1998

A Mechanically Checked Proof of the AMD5_K86^TM Floating Point Division Program.

J Strother Moore, Thomas W. Lynch, Matt Kaufmann

IEEE Trans. Computers, 1998

Design Constraints in Symbolic Model Checking.

Matt Kaufmann, Andrew Martin, Carl Pixley

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

ACL2 Support for Verification Projects (Invited Talk).

Matt Kaufmann

Proceedings of the Automated Deduction, 1998

1997

An Industrial Strength Theorem Prover for a Logic Based on Common Lisp.

Matt Kaufmann, J Strother Moore

IEEE Trans. Software Eng., 1997

Intertwined Development and Formal Verification of a 60x Bus Model.

Matt Kaufmann, Carl Pixley

Proceedings of the Proceedings 1997 International Conference on Computer Design: VLSI in Computers & Processors, 1997

Formal Verification of FIRE: A Case Study.

Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley

Proceedings of the 34st Conference on Design Automation, 1997

1996

Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem.

Matt Kaufmann, Paolo Pecchiari

J. Autom. Reason., 1996

Commercial Design Verification: Methodology and Tools.

Carl Pixley, Noel R. Strader, William C. Bruce, Jaehong Park, Matt Kaufmann, Kurt Shultz, Michael Burns, Jainendra Kumar, Jun Yuan, Janet Nguyen

Proceedings of the Proceedings IEEE International Test Conference 1996, 1996

ACL2 Theorems About Commercial Microprocessors.

Bishop Brock, Matt Kaufmann, J Strother Moore

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

1992

An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification.

Matt Kaufmann

J. Autom. Reason., 1992

1991

Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm.

Matt Kaufmann

J. Autom. Reason., 1991

An Informal Discussion of Issues in Mechanically-Assisted Reasoning.

Matt Kaufmann

Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, 1991

Functional Instantiation in First-Order Logic.

Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J Strother Moore

Proceedings of the Artificial and Mathematical Theory of Computation, 1991

1990

RCL: A Lisp Verification System.

Matt Kaufmann

Proceedings of the 10th International Conference on Automated Deduction, 1990

1988

An Interactive Enhancement to the Boyer-Moore Theorem Prover.

Matt Kaufmann

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

Remarks on Weak Notions of Saturation in Models of Peano Arithmetic.

Matt Kaufmann, James H. Schmerl

J. Symb. Log., 1987

1986

The Hanf number of stationary logic.

Matt Kaufmann, Saharon Shelah

Notre Dame J. Formal Log., 1986

1985

A prototype theorem-prover for a higher-order functional language.

Robert S. Boyer, Matt Kaufmann

ACM SIGSOFT Softw. Eng. Notes, 1985

A note on the Hanf number of second-order logic.

Matt Kaufmann

Notre Dame J. Formal Log., 1985

Meeting of the Association for Symbolic Logic: Notre Dame, Indiana, 1984.

John T. Baldwin, Matt Kaufmann, Julia F. Knight

J. Symb. Log., 1985

On random models of finite power and monadic logic.

Matt Kaufmann, Saharon Shelah

Discret. Math., 1985

1984

Some remarks on equivalence in infinitary and stationary logic.

Matt Kaufmann

Notre Dame J. Formal Log., 1984

Definable Ultrapowers and Ultrafilters over Admissible Ordinals.

Matt Kaufmann, Evangelos Kranakis

Math. Log. Q., 1984

Filter Logics on omega.

Matt Kaufmann

J. Symb. Log., 1984

The Strength of Nonstandard Methods in Arithmetic.

C. Ward Henson, Matt Kaufmann, H. Jerome Keisler

J. Symb. Log., 1984

A nonconservativity result on global choice.

Matt Kaufmann, Saharon Shelah

Ann. Pure Appl. Log., 1984

Saturation and simple extensions of models of peano arithmetic.

Matt Kaufmann, James H. Schmerl

Ann. Pure Appl. Log., 1984

1983

Blunt and Topless End Extensions of Models of Set Theory.

Matt Kaufmann

J. Symb. Log., 1983

Set Theory With a Filter Quantifier.

Matt Kaufmann

J. Symb. Log., 1983

1979

A New Omitting Types Theorem for L(Q).

Matt Kaufmann

J. Symb. Log., 1979