| A Hierarchical Approach to Self-Timed Circuit Verification | 1 | 0.37 | 2019 |
| Data-Loop-Free Self-Timed Circuit Verification | 1 | 0.37 | 2018 |
| Efficient, Verified Checking Of Propositional Proofs | 6 | 0.45 | 2017 |
| Efficient Certified RAT Verification. | 3 | 0.41 | 2017 |
| Expressing Symmetry Breaking in DRAT Proofs | 9 | 0.54 | 2015 |
| Fourier Series Formalization In Acl2(R) | 0 | 0.34 | 2015 |
| DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. | 34 | 1.10 | 2014 |
| Bridging the gap between easy generation and efficient verification of unsatisfiability proofs | 2 | 0.37 | 2014 |
| Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls | 5 | 0.53 | 2014 |
| Trimming while checking clausal proofs | 15 | 0.75 | 2013 |
| Abstract Stobjs And Their Application To Isa Modeling | 9 | 0.67 | 2013 |
| Automated Code Proofs on a Formal Model of the X86. | 3 | 0.53 | 2013 |
| A formal model of a large memory that supports efficient execution | 3 | 0.50 | 2012 |
| Using mathematics on an industrial scale. | 0 | 0.34 | 2010 |
| Verifying VIA Nano microprocessor components | 2 | 0.42 | 2010 |
| Connecting pre-silicon and post-silicon verification | 8 | 0.67 | 2009 |
| Centaur Technology Media Unit Verification | 16 | 1.21 | 2009 |
| Mechanized information flow analysis through inductive assertions | 2 | 0.38 | 2008 |
| A Mechanical Analysis of Program Verification Strategies | 4 | 0.49 | 2008 |
| Mechanized Certification of Secure Hardware Designs | 1 | 0.36 | 2007 |
| Function memoization and unique object representation for ACL2 functions | 11 | 0.86 | 2006 |
| A SAT-based procedure for verifying finite state machines in ACL2 | 2 | 0.41 | 2006 |
| Automatic Insertion of Low Power Annotations in RTL for Pipelined Microprocessors | 4 | 0.46 | 2006 |
| An embedding of the ACL2 logic in HOL | 8 | 0.86 | 2006 |
| Phylogenetic trees in ACL2 | 2 | 0.50 | 2006 |
| Verisym: Verifying Circuits by Symbolic Simulation | 0 | 0.34 | 2003 |
| Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings | 10 | 1.00 | 2003 |
| Industrial Practice of Formal Hardware Verification: A Sampling | 1 | 0.35 | 2003 |
| Verification of FM9801: An Out-of-Order Microprocessor Model with Speculative Execution, Exceptions, and Program-Modifying Capability | 17 | 0.84 | 2002 |
| Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, Texas, USA, November 1-3, 2000, Proceedings | 25 | 3.08 | 2000 |
| Hardware Modeling Using Function Encapsulation | 2 | 0.40 | 2000 |
| Results of the Verification of a Complex Pipelined Machine Model | 12 | 0.69 | 1999 |
| Verifying the FM9801 Microarchitecture | 13 | 0.83 | 1999 |
| Processor Verification with Precise Exeptions and Speculative Execution | 58 | 3.91 | 1998 |
| Formally specifying and mechanically verifying programs for the Motorola complex arithmetic processor DSP | 11 | 1.57 | 1997 |
| Trace Table Based Approach for Pipeline Microprocessor Verification | 40 | 4.50 | 1997 |
| The DUAL-EVAL Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor | 17 | 1.40 | 1997 |
| Introduction to a Formally Defined Hardware Description Language | 8 | 0.88 | 1992 |
| The verification of a bit-slice ALU | 10 | 1.05 | 1989 |
| Microprocessor design verification | 61 | 9.79 | 1989 |
| An approach to systems verification | 73 | 9.33 | 1989 |
| Toward Verified Execution Environments. | 11 | 5.33 | 1987 |
