Warren A. Hunt Jr.

Publication Activity (10 Years)

Years Active: 1987-2022
Publications (10 Years): 8

Top Topics

Boolean Optimization

Natural Language Learning

Symmetry Breaking

Top Venues

Publications

Warren A. Hunt Jr., Vivek Ramanathan, J. Strother Moore
VWSIM: A Circuit Simulator. ACL2 (2022)
Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland
A Hierarchical Approach to Self-Timed Circuit Verification. ASYNC (2019)
Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland
Data-Loop-Free Self-Timed Circuit Verification. ASYNC (2018)
Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler
Efficient, Verified Checking of Propositional Proofs. ITP (2017)
Cuong K. Chau, Warren A. Hunt Jr., Marly Roncken, Ivan E. Sutherland
A Framework for Asynchronous Circuit Modeling and Verification in ACL2. Haifa Verification Conference (2017)
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
How to think about self-timed systems. ACSSC (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)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Expressing Symmetry Breaking in DRAT Proofs. CADE (2015)
Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT (2014)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verification Reliab. 24 (8) (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)
Shilpi Goel, Warren A. Hunt Jr.
Automated Code Proofs on a Formal Model of the X86. VSTTE (2013)
Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
Mechanical Verification of SAT Refutations with Extended Resolution. ITP (2013)
David L. Rager, Warren A. Hunt Jr., Matt Kaufmann
A Parallelized Theorem Prover for a Logic with Parallel Execution. ITP (2013)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Trimming while checking clausal proofs. FMCAD (2013)
Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
Verifying Refutations with Extended Resolution. CADE (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)
Anna Slobodová, Jared Davis, Sol Swords, Warren A. Hunt Jr.
A flexible formal verification framework for industrial scale validation. MEMOCODE (2011)
Warren A. Hunt Jr.
Using mathematics on an industrial scale. ISAIM (2010)
Warren A. Hunt Jr.
Verifying VIA Nano microprocessor components. FMCAD (2010)
Sol Swords, Warren A. Hunt Jr.
A Mechanically Verified AIG-to-BDD Conversion Algorithm. ITP (2010)
Sandip Ray, Warren A. Hunt Jr.
Connecting pre-silicon and post-silicon verification. FMCAD (2009)
Warren A. Hunt Jr., Sol Swords
Centaur Technology Media Unit Verification. CAV (2009)
Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore
A Mechanical Analysis of Program Verification Strategies. J. Autom. Reason. 40 (4) (2008)
Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young
Mechanized Information Flow Analysis through Inductive Assertions. FMCAD (2008)
Sandip Ray, Warren A. Hunt Jr.
Mechanized Certification of Secure Hardware Designs. MTV (2007)
Vinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr.
Automatic insertion of low power annotations in RTL for pipelined microprocessors. DATE (2006)
Erik Reeber, Warren A. Hunt Jr.
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). IJCAR (2006)
Robert S. Boyer, Warren A. Hunt Jr.
Function memoization and unique object representation for ACL2 functions. ACL2 (2006)
Warren A. Hunt Jr., Erik Reeber
A SAT-based procedure for verifying finite state machines in ACL2. ACL2 (2006)
Warren A. Hunt Jr., Serita M. Nelesen
Phylogenetic trees 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)
Warren A. Hunt Jr., Erik Reeber
Formalization of the DE2 Language. CHARME (2005)
Robert S. Boyer, Warren A. Hunt Jr., Serita M. Nelesen
A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance. WABI (2005)
Warren A. Hunt Jr.
Mechanical Mathematical Methods for Microprocessor Verification. CAV (2004)
Sandip Ray, Warren A. Hunt Jr.
Deductive Verification of Pipelined Machines Using First-Order Quantification. CAV (2004)
Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore
Linear and Nonlinear Arithmetic in ACL2. CHARME (2003)
William Adams, Warren A. Hunt Jr., Damir Jamsek
Verisym: Verifying Circuits by Symbolic Simulation. Formal Methods Syst. Des. 22 (2) (2003)
Ganesh Gopalakrishnan, Warren A. Hunt Jr.
Industrial Practice of Formal Hardware Verification: A Sampling. Formal Methods Syst. Des. 22 (2) (2003)
Jun Sawada, Warren A. Hunt Jr.
Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability. Formal Methods Syst. Des. 20 (2) (2002)
Warren A. Hunt Jr.
Introduction: Special Issue on Microprocessor Verifications. Formal Methods Syst. Des. 20 (2) (2002)
Jun Sawada, Warren A. Hunt Jr.
Hardware Modeling Using Function Encapsulation. FMCAD (2000)
Jun Sawada, Warren A. Hunt Jr.
Results of the Verification of a Complex Pipelined Machine Model. CHARME (1999)
Warren A. Hunt Jr., Jun Sawada
Verifying the FM9801 microarchitecture. IEEE Micro 19 (3) (1999)
Jun Sawada, Warren A. Hunt Jr.
Processor Verification with Precise Exeptions and Speculative Execution. CAV (1998)
Bishop Brock, Warren A. Hunt Jr.
Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP. ICCD (1997)
Bishop Brock, Warren A. Hunt Jr.
The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor. Formal Methods Syst. Des. 11 (1) (1997)
Jun Sawada, Warren A. Hunt Jr.
Trace Table Based Approach for Pipeline Microprocessor Verification. CAV (1997)
Bishop Brock, Warren A. Hunt Jr., William D. Young
Introduction to a Formally Defined Hardware Description Language. TPCD (1992)
William R. Bevier, Warren A. Hunt Jr., J. Strother Moore, William D. Young
An Approach to Systems Verification. J. Autom. Reason. 5 (4) (1989)
Warren A. Hunt Jr., Bishop Brock
The Verification of a Bit-slice ALU. Hardware Specification, Verification and Synthesis (1989)
Warren A. Hunt Jr.
Microprocessor Design Verification. J. Autom. Reason. 5 (4) (1989)
William R. Bevier, Warren A. Hunt Jr., William D. Young
Toward Verified Execution Environments. IEEE Symposium on Security and Privacy (1987)