default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDWarren A. Hunt Jr.
Person information
- affiliation: University of Texas at Austin, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c49]Carl Kwan, Warren A. Hunt Jr.:
Formalizing the Cholesky Factorization Theorem. ITP 2024: 25:1-25:16- 2022
- [c48]Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore:
VWSIM: A Circuit Simulator. ACL2 2022: 61-75
2010 – 2019
- 2019
- [c47]Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland:
A Hierarchical Approach to Self-Timed Circuit Verification. ASYNC 2019: 105-113 - 2018
- [c46]Cuong K. Chau, Warren A. Hunt Jr., Matt Kaufmann, Marly Roncken, Ivan E. Sutherland:
Data-Loop-Free Self-Timed Circuit Verification. ASYNC 2018: 51-58 - 2017
- [c45]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: 1597-1604 - [c44]Luís Cruz-Filipe
, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp:
Efficient Certified RAT Verification. CADE 2017: 220-236 - [c43]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: 3-18 - [c42]Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler:
Efficient, Verified Checking of Propositional Proofs. ITP 2017: 269-284 - [p2]Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann:
Engineering a Formal, Executable x86 ISA Simulator for Software Verification. Provably Correct Systems 2017: 173-209 - [e3]Anna Slobodová, Warren A. Hunt Jr.:
Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017. EPTCS 249, 2017 [contents] - 2016
- [i1]Luís Cruz-Filipe, Marijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Peter Schneider-Kamp:
Efficient Certified RAT Verification. CoRR abs/1612.02353 (2016) - 2015
- [c41]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Expressing Symmetry Breaking in DRAT Proofs. CADE 2015: 591-606 - [c40]Cuong K. Chau, Matt Kaufmann, Warren A. Hunt Jr.:
Fourier Series Formalization in ACL2(r). ACL2 2015: 35-51 - 2014
- [j10]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): 593-607 (2014) - [c39]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: 91-98 - [c38]Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.:
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT 2014: 422-429 - 2013
- [c37]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Verifying Refutations with Extended Resolution. CADE 2013: 345-359 - [c36]Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler:
Trimming while checking clausal proofs. FMCAD 2013: 181-188 - [c35]Nathan Wetzler, Marijn Heule, Warren A. Hunt Jr.:
Mechanical Verification of SAT Refutations with Extended Resolution. ITP 2013: 229-244 - [c34]David L. Rager, Warren A. Hunt Jr., Matt Kaufmann:
A Parallelized Theorem Prover for a Logic with Parallel Execution. ITP 2013: 435-450 - [c33]Shilpi Goel, Warren A. Hunt Jr.:
Automated Code Proofs on a Formal Model of the X86. VSTTE 2013: 222-241 - [c32]Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann:
Abstract Stobjs and Their Application to ISA Modeling. ACL2 2013: 54-69 - 2012
- [c31]Warren A. Hunt Jr., Matt Kaufmann:
A formal model of a large memory that supports efficient execution. FMCAD 2012: 60-67 - 2011
- [c30]David L. Rager, Warren A. Hunt Jr., Matt Kaufmann:
A Futures Library and Parallelism Abstractions for a Functional Subset of Lisp. ELS 2011: 13-16 - [c29]Anna Slobodová, Jared Davis, Sol Swords, Warren A. Hunt Jr.:
A flexible formal verification framework for industrial scale validation. MEMOCODE 2011: 89-97 - 2010
- [c28]Warren A. Hunt Jr.:
Verifying VIA Nano microprocessor components. FMCAD 2010: 3-10 - [c27]Warren A. Hunt Jr.:
Using mathematics on an industrial scale. ISAIM 2010 - [c26]Sol Swords, Warren A. Hunt Jr.:
A Mechanically Verified AIG-to-BDD Conversion Algorithm. ITP 2010: 435-449 - [p1]Warren A. Hunt Jr., Sol Swords, Jared Davis, Anna Slobodová:
Use of Formal Verification at Centaur Technology. Design and Verification of Microprocessor Systems for High-Assurance Applications 2010: 65-88
2000 – 2009
- 2009
- [c25]Warren A. Hunt Jr., Sol Swords:
Centaur Technology Media Unit Verification. CAV 2009: 353-367 - [c24]Sandip Ray, Warren A. Hunt Jr.:
Connecting pre-silicon and post-silicon verification. FMCAD 2009: 160-163 - 2008
- [j9]Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore:
A Mechanical Analysis of Program Verification Strategies. J. Autom. Reason. 40(4): 245-269 (2008) - [c23]Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip Ray, William D. Young:
Mechanized Information Flow Analysis through Inductive Assertions. FMCAD 2008: 1-4 - 2007
- [c22]Sandip Ray, Warren A. Hunt Jr.:
Mechanized Certification of Secure Hardware Designs. MTV 2007: 25-32 - 2006
- [c21]Michael J. C. Gordon, Warren A. Hunt Jr., Matt Kaufmann, James Reynolds:
An embedding of the ACL2 logic in HOL. ACL2 2006: 40-46 - [c20]Robert S. Boyer, Warren A. Hunt Jr.:
Function memoization and unique object representation for ACL2 functions. ACL2 2006: 81-89 - [c19]Warren A. Hunt Jr., Serita M. Nelesen:
Phylogenetic trees in ACL2. ACL2 2006: 99-102 - [c18]Warren A. Hunt Jr., Erik Reeber:
A SAT-based procedure for verifying finite state machines in ACL2. ACL2 2006: 127-135 - [c17]Erik Reeber, Warren A. Hunt Jr.:
A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). IJCAR 2006: 453-467 - [c16]Vinod Viswanath, Jacob A. Abraham, Warren A. Hunt Jr.:
Automatic insertion of low power annotations in RTL for pipelined microprocessors. DATE 2006: 496-501 - [c15]Michael J. C. Gordon, James Reynolds, Warren A. Hunt Jr., Matt Kaufmann:
An Integration of HOL and ACL2. FMCAD 2006: 153-160 - 2005
- [c14]Warren A. Hunt Jr., Erik Reeber:
Formalization of the DE2 Language. CHARME 2005: 20-34 - [c13]Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith:
Meta Reasoning in ACL2. TPHOLs 2005: 163-178 - [c12]Robert S. Boyer, Warren A. Hunt Jr., Serita M. Nelesen:
A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance. WABI 2005: 353-364 - 2004
- [c11]Sandip Ray, Warren A. Hunt Jr.:
Deductive Verification of Pipelined Machines Using First-Order Quantification. CAV 2004: 31-43 - [c10]Warren A. Hunt Jr.:
Mechanical Mathematical Methods for Microprocessor Verification. CAV 2004: 523-533 - 2003
- [j8]Ganesh Gopalakrishnan, Warren A. Hunt Jr.:
Industrial Practice of Formal Hardware Verification: A Sampling. Formal Methods Syst. Des. 22(2): 95-99 (2003) - [j7]William Adams, Warren A. Hunt Jr., Damir Jamsek:
Verisym: Verifying Circuits by Symbolic Simulation. Formal Methods Syst. Des. 22(2): 163-173 (2003) - [c9]Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore:
Linear and Nonlinear Arithmetic in ACL2. CHARME 2003: 319-333 - [e2]Warren A. Hunt Jr., Fabio Somenzi:
Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. Lecture Notes in Computer Science 2725, Springer 2003, ISBN 3-540-40524-0 [contents] - 2002
- [j6]Warren A. Hunt Jr.:
Introduction: Special Issue on Microprocessor Verifications. Formal Methods Syst. Des. 20(2): 135-137 (2002) - [j5]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): 187-222 (2002) - 2000
- [c8]Jun Sawada, Warren A. Hunt Jr.:
Hardware Modeling Using Function Encapsulation. FMCAD 2000: 234-245 - [e1]Warren A. Hunt Jr., Steven D. Johnson:
Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings. Lecture Notes in Computer Science 1954, Springer 2000, ISBN 3-540-41219-0 [contents]
1990 – 1999
- 1999
- [j4]Warren A. Hunt Jr., Jun Sawada:
Verifying the FM9801 microarchitecture. IEEE Micro 19(3): 47-55 (1999) - [c7]Jun Sawada, Warren A. Hunt Jr.:
Results of the Verification of a Complex Pipelined Machine Model. CHARME 1999: 313-316 - 1998
- [c6]Jun Sawada, Warren A. Hunt Jr.:
Processor Verification with Precise Exeptions and Speculative Execution. CAV 1998: 135-146 - 1997
- [j3]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): 71-104 (1997) - [c5]Jun Sawada, Warren A. Hunt Jr.:
Trace Table Based Approach for Pipeline Microprocessor Verification. CAV 1997: 364-375 - [c4]Bishop Brock, Warren A. Hunt Jr.:
Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP. ICCD 1997: 31-36 - 1994
- [b1]Warren A. Hunt Jr.:
FM8501: A Verified Microprocessor. Lecture Notes in Computer Science 795, Springer 1994, ISBN 3-540-57960-5 - 1992
- [c3]Bishop Brock, Warren A. Hunt Jr., William D. Young:
Introduction to a Formally Defined Hardware Description Language. TPCD 1992: 3-35
1980 – 1989
- 1989
- [j2]William R. Bevier, Warren A. Hunt Jr., J Strother Moore, William D. Young:
An Approach to Systems Verification. J. Autom. Reason. 5(4): 411-428 (1989) - [j1]Warren A. Hunt Jr.:
Microprocessor Design Verification. J. Autom. Reason. 5(4): 429-460 (1989) - [c2]Warren A. Hunt Jr., Bishop Brock:
The Verification of a Bit-slice ALU. Hardware Specification, Verification and Synthesis 1989: 282-306 - 1987
- [c1]William R. Bevier, Warren A. Hunt Jr., William D. Young:
Toward Verified Execution Environments. S&P 1987: 106-115
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:10 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
