Warren A. Hunt Jr.

According to our database, Warren A. Hunt Jr. authored at least 62 papers between 1987 and 2024.

Collaborative distances:

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

2024

Formalizing the Cholesky Factorization Theorem.

Carl Kwan, Warren A. Hunt Jr.

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2022

VWSIM: A Circuit Simulator.

Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore

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

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

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

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

A Framework for Asynchronous Circuit Modeling and Verification in ACL2.

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

Proceedings of the Hardware and Software: Verification and Testing, 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

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

Proceedings of the 51st Asilomar Conference on Signals, Systems, and Computers, 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

Expressing Symmetry Breaking in DRAT Proofs.

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

Proceedings of the Automated Deduction - CADE-25, 2015

2014

Bridging the gap between easy generation and efficient verification of unsatisfiability proofs.

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

Softw. Test. Verification Reliab., 2014

DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs.

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

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2014, 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

Automated Code Proofs on a Formal Model of the X86.

Shilpi Goel, Warren A. Hunt Jr.

Proceedings of the Verified Software: Theories, Tools, Experiments, 2013

Mechanical Verification of SAT Refutations with Extended Resolution.

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

Proceedings of the Interactive Theorem Proving - 4th International Conference, 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

Trimming while checking clausal proofs.

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

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

Verifying Refutations with Extended Resolution.

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

Proceedings of the Automated Deduction - CADE-24, 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

A flexible formal verification framework for industrial scale validation.

Anna Slobodová, Jared Davis, Sol Swords, Warren A. Hunt Jr.

Proceedings of the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign, 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

A Mechanically Verified AIG-to-BDD Conversion Algorithm.

Sol Swords, Warren A. Hunt Jr.

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Using mathematics on an industrial scale.

Warren A. Hunt Jr.

Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2010

Verifying VIA Nano microprocessor components.

Warren A. Hunt Jr.

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Use of Formal Verification at Centaur Technology.

Warren A. Hunt Jr., Sol Swords, Jared Davis, Anna Slobodová

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

2009

Connecting pre-silicon and post-silicon verification.

Sandip Ray, Warren A. Hunt Jr.

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

Centaur Technology Media Unit Verification.

Warren A. Hunt Jr., Sol Swords

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

A Mechanical Analysis of Program Verification Strategies.

Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore

J. Autom. Reason., 2008

Mechanized Information Flow Analysis through Inductive Assertions.

Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young

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

2007

Mechanized Certification of Secure Hardware Designs.

Sandip Ray, Warren A. Hunt Jr.

Proceedings of the Eighth International Workshop on Microprocessor Test and Verification (MTV 2007), 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

Automatic insertion of low power annotations in RTL for pipelined microprocessors.

Vinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr.

Proceedings of the Conference on Design, Automation and Test in Europe, 2006

A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA).

Erik Reeber, Warren A. Hunt Jr.

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

A SAT-based procedure for verifying finite state machines in ACL2.

Warren A. Hunt Jr., Erik Reeber

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

Phylogenetic trees in ACL2.

Warren A. Hunt Jr., Serita M. Nelesen

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

Function memoization and unique object representation for ACL2 functions.

Robert S. Boyer, Warren A. Hunt Jr.

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

2005

A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance.

Robert S. Boyer, Warren A. Hunt Jr., Serita M. Nelesen

Proceedings of the Algorithms in Bioinformatics, 5th International Workshop, 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

Formalization of the DE2 Language.

Warren A. Hunt Jr., Erik Reeber

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Deductive Verification of Pipelined Machines Using First-Order Quantification.

Sandip Ray, Warren A. Hunt Jr.

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

Mechanical Mathematical Methods for Microprocessor Verification.

Warren A. Hunt Jr.

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Industrial Practice of Formal Hardware Verification: A Sampling.

Ganesh Gopalakrishnan, Warren A. Hunt Jr.

Formal Methods Syst. Des., 2003

Verisym: Verifying Circuits by Symbolic Simulation.

William Adams, Warren A. Hunt Jr., Damir Jamsek

Formal Methods Syst. Des., 2003

Linear and Nonlinear Arithmetic in ACL2.

Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability.

Jun Sawada, Warren A. Hunt Jr.

Formal Methods Syst. Des., 2002

Introduction: Special Issue on Microprocessor Verifications.

Warren A. Hunt Jr.

Formal Methods Syst. Des., 2002

2000

Hardware Modeling Using Function Encapsulation.

Jun Sawada, Warren A. Hunt Jr.

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

1999

Verifying the FM9801 microarchitecture.

Warren A. Hunt Jr., Jun Sawada

IEEE Micro, 1999

Results of the Verification of a Complex Pipelined Machine Model.

Jun Sawada, Warren A. Hunt Jr.

Proceedings of the Correct Hardware Design and Verification Methods, 1999

1998

Processor Verification with Precise Exeptions and Speculative Execution.

Jun Sawada, Warren A. Hunt Jr.

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

1997

The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor.

Bishop Brock, Warren A. Hunt Jr.

Formal Methods Syst. Des., 1997

Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP.

Bishop Brock, Warren A. Hunt Jr.

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

Trace Table Based Approach for Pipeline Microprocessor Verification.

Jun Sawada, Warren A. Hunt Jr.

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1994

FM8501: A Verified Microprocessor

Warren A. Hunt Jr.

Lecture Notes in Computer Science 795, Springer, ISBN: 3-540-57960-5, 1994

1992

Introduction to a Formally Defined Hardware Description Language.

Bishop Brock, Warren A. Hunt Jr., William D. Young

Proceedings of the Theorem Provers in Circuit Design, 1992

1989

Microprocessor Design Verification.

Warren A. Hunt Jr.

J. Autom. Reason., 1989

An Approach to Systems Verification.

William R. Bevier, Warren A. Hunt Jr., J Strother Moore, William D. Young

J. Autom. Reason., 1989

The Verification of a Bit-slice ALU.

Warren A. Hunt Jr., Bishop Brock

Proceedings of the Hardware Specification, 1989

1987

Toward Verified Execution Environments.

William R. Bevier, Warren A. Hunt Jr., William D. Young

Proceedings of the 1987 IEEE Symposium on Security and Privacy, 1987