| 2025 | FMCAD | A Method for the Verification of Memory Management Software in the Presence of TLBs. | Yahya Sohail, Warren A. Hunt Jr. |
| 2024 | FMCAD | Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms. | Carl Kwan, Warren A. Hunt Jr. |
| 2024 | ITP | Formalizing the Cholesky Factorization Theorem. | Carl Kwan, Warren A. Hunt Jr. |
| 2017 | ACSSC | How to think about self-timed systems. | Marly Roncken, Ivan E. Sutherland, Chris Chen, Yong Hei, Warren A. Hunt Jr., Cuong K. Chau, Swetha Mettala Gilla, Hoon Park, Xiaoyu Song, Anping He, Hong Chen |
| 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 |
| 2015 | CADE | Expressing Symmetry Breaking in DRAT Proofs. | Marijn Heule, Warren A. Hunt Jr., 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 | SAT | DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. | Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
| 2013 | CADE | Verifying Refutations with Extended Resolution. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | FMCAD | Trimming while checking clausal proofs. | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
| 2013 | ITP | A Parallelized Theorem Prover for a Logic with Parallel Execution. | David L. Rager, Warren A. Hunt Jr., Matt Kaufmann |
| 2013 | ITP | Mechanical Verification of SAT Refutations with Extended Resolution. | Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr. |
| 2012 | FMCAD | A formal model of a large memory that supports efficient execution. | Warren A. Hunt Jr., Matt Kaufmann |
| 2011 | MEMOCODE | A flexible formal verification framework for industrial scale validation. | Anna Slobodov, Jared Davis, Sol Swords, Warren A. Hunt Jr. |
| 2010 | FMCAD | Verifying VIA Nano microprocessor components. | Warren A. Hunt Jr. |
| 2010 | ISAIM | Using mathematics on an industrial scale. | Warren A. Hunt Jr. |
| 2010 | ITP | A Mechanically Verified AIG-to-BDD Conversion Algorithm. | Sol Swords, Warren A. Hunt Jr. |
| 2009 | CAV | Centaur Technology Media Unit Verification. | Warren A. Hunt Jr., Sol Swords |
| 2009 | FMCAD | Connecting pre-silicon and post-silicon verification. | Sandip Ray, Warren A. Hunt Jr. |
| 2008 | FMCAD | Mechanized Information Flow Analysis through Inductive Assertions. | Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young |
| 2006 | CADE | A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). | Erik Reeber, Warren A. Hunt Jr. |
| 2006 | DATE | Automatic insertion of low power annotations in RTL for pipelined microprocessors. | Vinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr. |
| 2006 | FMCAD | An Integration of HOL and ACL2. | Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann |
| 2005 | WABI | A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance. | Robert S. Boyer, Warren A. Hunt Jr., Serita M. Nelesen |
| 2004 | CAV | Mechanical Mathematical Methods for Microprocessor Verification. | Warren A. Hunt Jr. |
| 2004 | CAV | Deductive Verification of Pipelined Machines Using First-Order Quantification. | Sandip Ray, Warren A. Hunt Jr. |
| 2000 | FMCAD | Hardware Modeling Using Function Encapsulation. | Jun Sawada, Warren A. Hunt Jr. |
| 1998 | CAV | Processor Verification with Precise Exeptions and Speculative Execution. | Jun Sawada, Warren A. Hunt Jr. |
| 1997 | CAV | Trace Table Based Approach for Pipeline Microprocessor Verification. | Jun Sawada, Warren A. Hunt Jr. |
| 1997 | ICCD | Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP. | Bishop Brock, Warren A. Hunt Jr. |
| 1987 | SP | Toward Verified Execution Environments. | William R. Bevier, Warren A. Hunt Jr., William D. Young |