| 2017 | CADE | Efficient Certified RAT Verification. | Lus Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp |
| 2017 | ITP | Efficient, Verified Checking of Propositional Proofs. | Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler |
| 2014 | FMCAD | Simulation and formal verification of x86 machine-code programs that make system calls. | Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh |
| 2014 | ITP | Rough Diamond: An Extension of Equivalence-Based Rewriting. | Matt Kaufmann, J Strother Moore |
| 2013 | ITP | A Parallelized Theorem Prover for a Logic with Parallel Execution. | David L. Rager, Warren A. Hunt Jr., Matt Kaufmann |
| 2012 | FMCAD | A formal model of a large memory that supports efficient execution. | Warren A. Hunt Jr., Matt Kaufmann |
| 2006 | FMCAD | An Integration of HOL and ACL2. | Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann |
| 1998 | CADE | ACL2 Support for Verification Projects (Invited Talk). | Matt Kaufmann |
| 1998 | CAV | Design Constraints in Symbolic Model Checking. | Matt Kaufmann, Andrew Martin, Carl Pixley |
| 1997 | DAC | Formal Verification of FIRE: A Case Study. | Jae-Young Jang, Shaz Qadeer, Matt Kaufmann, Carl Pixley |
| 1997 | ICCD | Intertwined Development and Formal Verification of a 60x Bus Model. | Matt Kaufmann, Carl Pixley |
| 1996 | FMCAD | ACL2 Theorems About Commercial Microprocessors. | Bishop Brock, Matt Kaufmann, J Strother Moore |
| 1996 | ITC | 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 |
| 1990 | CADE | RCL: A Lisp Verification System. | Matt Kaufmann |
| 1988 | CADE | An Interactive Enhancement to the Boyer-Moore Theorem Prover. | Matt Kaufmann |