Matt Kaufmann - RankMe

76 papers A* 2A 5B 8C 1Journal 31Unranked 24

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	Extended Abstract: Mutable Objects with Several Implementations. ACL2 Matt Kaufmann, Yahya Sohail, Warren A. Hunt Jr.
2025	—	`conf`	Extended Abstract: Partial-encapsulate and Its Support for Floating-point Operations in ACL2. ACL2 Matt Kaufmann, J Strother Moore
2024	—	`ch.`	ACL2 Support for Floating-Point Computations. The Practice of Formal Methods (I) Matt Kaufmann, J Strother Moore
2023	—	`conf`	Advances in ACL2 Proof Debugging Tools. ACL2 Matt Kaufmann, J Strother Moore
2020	—	`conf`	Iteration in ACL2. ACL2 Matt Kaufmann, J Strother Moore
2020	J	`jnl`	Limited Second-Order Functionality in a First-Order Setting. J. Autom. Reason. Matt Kaufmann, J Strother Moore
2019	—	`conf`	A Hierarchical Approach to Self-Timed Circuit Verification. ASYNC Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland
2018	—	`conf`	Data-Loop-Free Self-Timed Circuit Verification. ASYNC Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland
2018	—	`conf`	DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract). ACL2 Matt Kaufmann
2018	J	`jnl`	Iterated ultrapowers for the masses. Arch. Math. Log. Ali Enayat, Matt Kaufmann, Zachiri McKenzie
2018	J	`jnl`	Largest initial segments pointwise fixed by automorphisms of models of set theory. Arch. Math. Log. Ali Enayat, Matt Kaufmann, Zachiri McKenzie
2018	—	`ed.`	Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, November 5-6, 2018. ACL2 Shilpi Goel, Matt Kaufmann
2017	—	`conf`	A Versatile, Sound Tool for Simplifying Definitions. ACL2 Alessandro Coglio, Matt Kaufmann, Eric Whitman Smith
2017	A	`conf`	Efficient Certified RAT Verification. CADE Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
2017	B	`conf`	Efficient, Verified Checking of Propositional Proofs. ITP Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler
2017	—	`ch.`	Engineering a Formal, Executable x86 ISA Simulator for Software Verification. Provably Correct Systems Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann
2017	—	`conf`	Meta-extract: Using Existing Facts in Meta-reasoning. ACL2 Matt Kaufmann, Sol Swords
2016	J	`jnl`	Efficient Certified RAT Verification. CoRR Luís Cruz-Filipe, Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
2015	—	`conf`	Fourier Series Formalization in ACL2(r). ACL2 Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.
2015	—	`ed.`	Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015. ACL2 Matt Kaufmann, David L. Rager
2014	—	`conf`	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. ACL2 Matt Kaufmann, J Strother Moore
2014	—	`conf`	Industrial-Strength Documentation for ACL2. ACL2 Jared Davis, Matt Kaufmann
2014	B	`conf`	Rough Diamond: An Extension of Equivalence-Based Rewriting. ITP Matt Kaufmann, J Strother Moore
2014	B	`conf`	Simulation and formal verification of x86 machine-code programs that make system calls. FMCAD Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh
2013	B	`conf`	A Parallelized Theorem Prover for a Logic with Parallel Execution. ITP David L. Rager, Warren A. Hunt Jr., Matt Kaufmann
2013	—	`conf`	Abstract Stobjs and Their Application to ISA Modeling ACL2 Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann
2013	—	`conf`	Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 ACL2 Matt Kaufmann, J Strother Moore
2012	B	`conf`	A formal model of a large memory that supports efficient execution. FMCAD Warren A. Hunt Jr., Matt Kaufmann
2011	—	`conf`	A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp. ELS David L. Rager, Warren A. Hunt Jr., Matt Kaufmann
2011	—	`conf`	How Can I Do That with ACL2? Recent Enhancements to ACL2 ACL2 Matt Kaufmann, J Strother Moore
2011	—	`conf`	Integrating Testing and Interactive Theorem Proving ACL2 Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, Panagiotis Manolios
2011	J	`jnl`	The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. J. Autom. Reason. Michael J. C. Gordon, Matt Kaufmann, Sandip Ray
2010	—	`ch.`	ACL2 and Its Applications to Digital System Verification. Design and Verification of Microprocessor Systems for High-Assurance Applications Matt Kaufmann, J Strother Moore
2010	B	`ed.`	Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings ITP Matt Kaufmann, Lawrence C. Paulson
2009	J	`jnl`	Integrating external deduction tools with ACL2. J. Appl. Log. Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber
2008	—	`conf`	An ACL2 Tutorial. TPHOLs Matt Kaufmann, J Strother Moore
2008	J	`jnl`	Efficient execution in an automated reasoning environment. J. Funct. Program. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding
2008	J	`jnl`	Rewriting with Equivalence Relations in ACL2. J. Autom. Reason. Bishop Brock, Matt Kaufmann, J Strother Moore
2007	—	`conf`	Proof Pearl: Wellfounded Induction on the Ordinals Up to TPHOLs Matt Kaufmann, Konrad Slind
2006	B	`conf`	An Integration of HOL and ACL2. FMCAD Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann
2006	—	`conf`	An embedding of the ACL2 logic in HOL. ACL2 Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds
2006	—	`conf`	Double rewriting for equivalential reasoning in ACL2. ACL2 Matt Kaufmann, J Strother Moore
2005	—	`conf`	Meta Reasoning in ACL2. TPHOLs Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
2001	J	`jnl`	Nonstandard Analysis in ACL2. J. Autom. Reason. Ruben Gamboa, Matt Kaufmann
2001	J	`jnl`	Structured Theory Development for a Mechanized Logic. J. Autom. Reason. Matt Kaufmann, J Strother Moore
2000	J	`jnl`	Verification of Year 2000 conversion rules using the ACL2 theorem prover. Int. J. Softw. Tools Technol. Transf. Matt Kaufmann
1998	J	`jnl`	A Mechanically Checked Proof of the AMD5 IEEE Trans. Computers J Strother Moore, Thomas W. Lynch, Matt Kaufmann
1998	A	`conf`	ACL2 Support for Verification Projects (Invited Talk). CADE Matt Kaufmann
1998	A*	`conf`	Design Constraints in Symbolic Model Checking. CAV Matt Kaufmann, Andrew Martin, Carl Pixley
1997	J	`jnl`	An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. Matt Kaufmann, J Strother Moore
1997	A*	`conf`	Formal Verification of FIRE: A Case Study. DAC Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley
1997	C	`conf`	Intertwined Development and Formal Verification of a 60x Bus Model. ICCD Matt Kaufmann, Carl Pixley
1996	B	`conf`	ACL2 Theorems About Commercial Microprocessors. FMCAD Bishop Brock, Matt Kaufmann, J Strother Moore
1996	A	`conf`	Commercial Design Verification: Methodology and Tools. ITC Carl Pixley, Noel R. Strader, William C. Bruce, Jaehong Park, Matt Kaufmann, Kurt Shultz, Michael Burns, Jainendra Kumar, Jun Yuan, Janet Nguyen
1996	J	`jnl`	Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem. J. Autom. Reason. Matt Kaufmann, Paolo Pecchiari
1992	J	`jnl`	An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. J. Autom. Reason. Matt Kaufmann
1991	—	`conf`	An Informal Discussion of Issues in Mechanically-Assisted Reasoning. TPHOLs Matt Kaufmann
1991	—	`conf`	Functional Instantiation in First-Order Logic. Artificial and Mathematical Theory of Computation Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J Strother Moore
1991	J	`jnl`	Generalization in the Presence of Free Variables: A Mechanically-Checked Correctness Proof for one Algorithm. J. Autom. Reason. Matt Kaufmann
1990	A	`conf`	RCL: A Lisp Verification System. CADE Matt Kaufmann
1988	A	`conf`	An Interactive Enhancement to the Boyer-Moore Theorem Prover. CADE Matt Kaufmann
1987	J	`jnl`	Remarks on Weak Notions of Saturation in Models of Peano Arithmetic. J. Symb. Log. Matt Kaufmann, James H. Schmerl
1986	J	`jnl`	The Hanf number of stationary logic. Notre Dame J. Formal Log. Matt Kaufmann, Saharon Shelah
1985	J	`jnl`	A note on the Hanf number of second-order logic. Notre Dame J. Formal Log. Matt Kaufmann
1985	J	`jnl`	A prototype theorem-prover for a higher-order functional language. ACM SIGSOFT Softw. Eng. Notes Robert S. Boyer, Matt Kaufmann
1985	J	`jnl`	Meeting of the Association for Symbolic Logic: Notre Dame, Indiana, 1984. J. Symb. Log. John T. Baldwin, Matt Kaufmann, Julia F. Knight
1985	J	`jnl`	On random models of finite power and monadic logic. Discret. Math. Matt Kaufmann, Saharon Shelah
1984	J	`jnl`	A nonconservativity result on global choice. Ann. Pure Appl. Log. Matt Kaufmann, Saharon Shelah
1984	J	`jnl`	Definable Ultrapowers and Ultrafilters over Admissible Ordinals. Math. Log. Q. Matt Kaufmann, Evangelos Kranakis
1984	J	`jnl`	Filter Logics on omega. J. Symb. Log. Matt Kaufmann
1984	J	`jnl`	Saturation and simple extensions of models of peano arithmetic. Ann. Pure Appl. Log. Matt Kaufmann, James H. Schmerl
1984	J	`jnl`	Some remarks on equivalence in infinitary and stationary logic. Notre Dame J. Formal Log. Matt Kaufmann
1984	J	`jnl`	The Strength of Nonstandard Methods in Arithmetic. J. Symb. Log. C. Ward Henson, Matt Kaufmann, H. Jerome Keisler
1983	J	`jnl`	Blunt and Topless End Extensions of Models of Set Theory. J. Symb. Log. Matt Kaufmann
1983	J	`jnl`	Set Theory With a Filter Quantifier. J. Symb. Log. Matt Kaufmann
1979	J	`jnl`	A New Omitting Types Theorem for L(Q). J. Symb. Log. Matt Kaufmann