| FM8501: A Verified Microprocessor, volume 795 of Lecture Notes in Artificial Intelligence WA Hunt Jr Springer-Verlag, Berlin, 1994 | 403* | 1994 |
| DRAT-trim: Efficient checking and trimming using expressive clausal proofs N Wetzler, MJH Heule, WA Hunt Jr International Conference on Theory and Applications of Satisfiability …, 2014 | 328 | 2014 |
| An approach to systems verification WR Bevier, WA Hunt, JS Moore, WD Young Journal of Automated Reasoning 5 (4), 411-428, 1989 | 234 | 1989 |
| Microprocessor design verification WA Hunt Journal of Automated Reasoning 5 (4), 429-460, 1989 | 221 | 1989 |
| Trimming while checking clausal proofs MJH Heule, WA Hunt, N Wetzler Formal Methods in Computer-Aided Design (FMCAD), 2013, 181-188, 2013 | 177 | 2013 |
| Processor verification with precise exceptions and speculative execution J Sawada, W Hunt Computer Aided Verification, 135-146, 1998 | 148 | 1998 |
| Efficient certified RAT verification L Cruz-Filipe, MJH Heule, WA Hunt, M Kaufmann, P Schneider-Kamp Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017 | 144 | 2017 |
| Verifying refutations with extended resolution MJH Heule, WA Hunt Jr, N Wetzler International Conference on Automated Deduction, 345-359, 2013 | 123 | 2013 |
| A formal HDL and its use in the FM9001 verification WA Hunt, BC Brock Philosophical Transactions of the Royal Society of London A: Mathematical …, 1992 | 116 | 1992 |
| The mechanical verification of a microprocessor design WA Hunt From HDL descriptions to guaranteed correct circuit designs, 89-129, 1987 | 108 | 1987 |
| Trace table based approach for pipelined microprocessor verification J Sawada, W Hunt Computer Aided Verification, 364-375, 1997 | 98 | 1997 |
| Efficient, Verified Checking of Propositional Proofs⋆ M Heule, W Hunt Jr, M Kaufmann, N Wetzler | 68* | |
| Industrial Hardware and Software Verification with ACL2 WA Hunt Jr, M Kaufmann, JS Moore, A Slobodova Philosophical Transactions of the Royal Society (Article Number 20150399 …, 2017 | 60 | 2017 |
| Simulation and formal verification of x86 machine-code programs that make system calls S Goel, WA Hunt, M Kaufmann, S Ghosh 2014 Formal Methods in Computer-Aided Design (FMCAD), 91-98, 2014 | 59 | 2014 |
| The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor WA Hunt Jr, BC Brock Design Automation Conference, 1995. Proceedings of the ASP-DAC'95/CHDL'95 …, 0 | 57* | |
| A flexible formal verification framework for industrial scale validation A Slobodová, J Davis, S Swords, W Hunt Formal Methods and Models for Codesign (MEMOCODE), 2011 9th IEEE/ACM …, 2011 | 56 | 2011 |
| The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor BC Brock, WA Hunt Formal Methods in System Design 11 (1), 71-104, 1997 | 55 | 1997 |
| Expressing symmetry breaking in DRAT proofs MJH Heule, WA Hunt Jr, N Wetzler International Conference on Automated Deduction, 591-606, 2015 | 52 | 2015 |
| Report on the formal specification and partial verification of the VIPER microprocessor B Brock, WA Hunt Jr Computer Assurance, 1991. COMPASS'91, Systems Integrity, Software Safety and …, 1991 | 49 | 1991 |
| Linear and nonlinear arithmetic in ACL2 W Hunt, R Krug, J Moore Correct Hardware Design and Verification Methods, 319-333, 2003 | 46 | 2003 |
Marijn HeuleAssociate Professor of Computer Science, Carnegie Mellon UniversityVerified email at cs.cmu.edu
