FM8501: A Verified Microprocessor, volume 795 of Lecture Notes in Artificial Intelligence WA Hunt Jr Springer-Verlag, Berlin, 1994 | 400* | 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 | 275 | 2014 |
An approach to systems verification WR Bevier, WA Hunt, JS Moore, WD Young Journal of Automated Reasoning 5 (4), 411-428, 1989 | 227 | 1989 |
Microprocessor design verification WA Hunt Journal of Automated Reasoning 5 (4), 429-460, 1989 | 215 | 1989 |
Trimming while checking clausal proofs MJH Heule, WA Hunt, N Wetzler Formal Methods in Computer-Aided Design (FMCAD), 2013, 181-188, 2013 | 153 | 2013 |
Processor verification with precise exceptions and speculative execution J Sawada, W Hunt Computer Aided Verification, 135-146, 1998 | 143 | 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 | 115 | 2017 |
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 | 115 | 1992 |
The mechanical verification of a microprocessor design WA Hunt From HDL descriptions to guaranteed correct circuit designs, 89-129, 1987 | 112 | 1987 |
Verifying refutations with extended resolution MJH Heule, WA Hunt Jr, N Wetzler International Conference on Automated Deduction, 345-359, 2013 | 105 | 2013 |
Trace table based approach for pipelined microprocessor verification J Sawada, W Hunt Computer Aided Verification, 364-375, 1997 | 93 | 1997 |
Efficient, Verified Checking of Propositional Proofs⋆ M Heule, W Hunt Jr, M Kaufmann, N Wetzler | 60* | |
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 | 59 | 2011 |
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 | 58* | |
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 | 56 | 1997 |
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 | 55 | 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 | 53 | 2014 |
Expressing symmetry breaking in DRAT proofs MJH Heule, WA Hunt Jr, N Wetzler International Conference on Automated Deduction, 591-606, 2015 | 48 | 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 | 47 | 1991 |
Linear and nonlinear arithmetic in ACL2 W Hunt, R Krug, J Moore Correct Hardware Design and Verification Methods, 319-333, 2003 | 45 | 2003 |