Warren A. Hunt Jr.

69 papers A* 6A 6B 16C 3Misc 2Journal 11Unranked 21

Year	Rank	Type	Title / Venue / Authors
2025	B	`conf`	A Method for the Verification of Memory Management Software in the Presence of TLBs. FMCAD Yahya Sohail, Warren A. Hunt Jr.
2025	—	`conf`	Extended Abstract: Mutable Objects with Several Implementations. ACL2 Matt Kaufmann, Yahya Sohail, Warren A. Hunt Jr.
2024	B	`conf`	Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms. FMCAD Carl Kwan, Warren A. Hunt Jr.
2024	B	`conf`	Formalizing the Cholesky Factorization Theorem. ITP Carl Kwan, Warren A. Hunt Jr.
2022	—	`conf`	VWSIM: A Circuit Simulator. ACL2 Warren A. Hunt Jr., Vivek Ramanathan, 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
2017	—	`conf`	A Framework for Asynchronous Circuit Modeling and Verification in ACL2. Haifa Verification Conference Cuong K. Chau, Warren A. Hunt Jr., Marly Roncken, Ivan E. Sutherland
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	Misc	`conf`	How to think about self-timed systems. ACSSC 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	—	`ed.`	Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017. ACL2 Anna Slobodová, Warren A. Hunt Jr.
2016	J	`jnl`	Efficient Certified RAT Verification. CoRR Luís Cruz-Filipe, Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp
2015	A	`conf`	Expressing Symmetry Breaking in DRAT Proofs. CADE Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
2015	—	`conf`	Fourier Series Formalization in ACL2(r). ACL2 Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.
2014	J	`jnl`	Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verification Reliab. Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
2014	A	`conf`	DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
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`	Automated Code Proofs on a Formal Model of the X86. VSTTE Shilpi Goel, Warren A. Hunt Jr.
2013	B	`conf`	Mechanical Verification of SAT Refutations with Extended Resolution. ITP Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.
2013	B	`conf`	Trimming while checking clausal proofs. FMCAD Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
2013	A	`conf`	Verifying Refutations with Extended Resolution. CADE Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler
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	C	`conf`	A flexible formal verification framework for industrial scale validation. MEMOCODE Anna Slobodová, Jared Davis, Sol Swords, Warren A. Hunt Jr.
2010	B	`conf`	A Mechanically Verified AIG-to-BDD Conversion Algorithm. ITP Sol Swords, Warren A. Hunt Jr.
2010	—	`ch.`	Use of Formal Verification at Centaur Technology. Design and Verification of Microprocessor Systems for High-Assurance Applications Warren A. Hunt Jr., Sol Swords, Jared Davis, Anna Slobodová
2010	Misc	`conf`	Using mathematics on an industrial scale. ISAIM Warren A. Hunt Jr.
2010	B	`conf`	Verifying VIA Nano microprocessor components. FMCAD Warren A. Hunt Jr.
2009	A*	`conf`	Centaur Technology Media Unit Verification. CAV Warren A. Hunt Jr., Sol Swords
2009	B	`conf`	Connecting pre-silicon and post-silicon verification. FMCAD Sandip Ray, Warren A. Hunt Jr.
2008	J	`jnl`	A Mechanical Analysis of Program Verification Strategies. J. Autom. Reason. Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore
2008	B	`conf`	Mechanized Information Flow Analysis through Inductive Assertions. FMCAD Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young
2007	—	`conf`	Mechanized Certification of Secure Hardware Designs. MTV Sandip Ray, Warren A. Hunt Jr.
2006	A	`conf`	A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). IJCAR Erik Reeber, Warren A. Hunt Jr.
2006	—	`conf`	A SAT-based procedure for verifying finite state machines in ACL2. ACL2 Warren A. Hunt Jr., Erik Reeber
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	A	`conf`	Automatic insertion of low power annotations in RTL for pipelined microprocessors. DATE Vinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr.
2006	—	`conf`	Function memoization and unique object representation for ACL2 functions. ACL2 Robert S. Boyer, Warren A. Hunt Jr.
2006	—	`conf`	Phylogenetic trees in ACL2. ACL2 Warren A. Hunt Jr., Serita M. Nelesen
2005	C	`conf`	A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance. WABI Robert S. Boyer, Warren A. Hunt Jr., Serita M. Nelesen
2005	—	`conf`	Formalization of the DE2 Language. CHARME Warren A. Hunt Jr., Erik Reeber
2005	—	`conf`	Meta Reasoning in ACL2. TPHOLs Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
2004	A*	`conf`	Deductive Verification of Pipelined Machines Using First-Order Quantification. CAV Sandip Ray, Warren A. Hunt Jr.
2004	A*	`conf`	Mechanical Mathematical Methods for Microprocessor Verification. CAV Warren A. Hunt Jr.
2003	A*	`ed.`	Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings CAV Warren A. Hunt Jr., Fabio Somenzi
2003	J	`jnl`	Industrial Practice of Formal Hardware Verification: A Sampling. Formal Methods Syst. Des. Ganesh Gopalakrishnan, Warren A. Hunt Jr.
2003	—	`conf`	Linear and Nonlinear Arithmetic in ACL2. CHARME Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore
2003	J	`jnl`	Verisym: Verifying Circuits by Symbolic Simulation. Formal Methods Syst. Des. William Adams, Warren A. Hunt Jr., Damir Jamsek
2002	J	`jnl`	Introduction: Special Issue on Microprocessor Verifications. Formal Methods Syst. Des. Warren A. Hunt Jr.
2002	J	`jnl`	Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability. Formal Methods Syst. Des. Jun Sawada, Warren A. Hunt Jr.
2000	B	`ed.`	Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings FMCAD Warren A. Hunt Jr., Steven D. Johnson
2000	B	`conf`	Hardware Modeling Using Function Encapsulation. FMCAD Jun Sawada, Warren A. Hunt Jr.
1999	—	`conf`	Results of the Verification of a Complex Pipelined Machine Model. CHARME Jun Sawada, Warren A. Hunt Jr.
1999	J	`jnl`	Verifying the FM9801 microarchitecture. IEEE Micro Warren A. Hunt Jr., Jun Sawada
1998	A*	`conf`	Processor Verification with Precise Exeptions and Speculative Execution. CAV Jun Sawada, Warren A. Hunt Jr.
1997	C	`conf`	Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP. ICCD Bishop Brock, Warren A. Hunt Jr.
1997	J	`jnl`	The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor. Formal Methods Syst. Des. Bishop Brock, Warren A. Hunt Jr.
1997	A*	`conf`	Trace Table Based Approach for Pipeline Microprocessor Verification. CAV Jun Sawada, Warren A. Hunt Jr.
1994	—	`book`	FM8501: A Verified Microprocessor Warren A. Hunt Jr.
1992	—	`conf`	Introduction to a Formally Defined Hardware Description Language. TPCD Bishop Brock, Warren A. Hunt Jr., William D. Young
1989	J	`jnl`	An Approach to Systems Verification. J. Autom. Reason. William R. Bevier, Warren A. Hunt Jr., J Strother Moore, William D. Young
1989	J	`jnl`	Microprocessor Design Verification. J. Autom. Reason. Warren A. Hunt Jr.
1989	—	`conf`	The Verification of a Bit-slice ALU. Hardware Specification, Verification and Synthesis Warren A. Hunt Jr., Bishop Brock
1987	—	`conf`	Toward Verified Execution Environments. S&P William R. Bevier, Warren A. Hunt Jr., William D. Young