| Limited Second-Order Functionality in a First-Order Setting | 0 | 0.34 | 2020 |
| A Hierarchical Approach to Self-Timed Circuit Verification | 1 | 0.37 | 2019 |
| Enhancements To Acl2 In Versions 5.0, 6.0, And 6.1 | 2 | 0.41 | 2013 |
| How Can I Do That With Acl2? Recent Enhancements To Acl2 | 4 | 0.88 | 2011 |
| Integrating external deduction tools with ACL2 | 8 | 0.59 | 2009 |
| An ACL2 Tutorial | 5 | 0.48 | 2008 |
| Structured Theory Development for a Mechanized Logic | 39 | 2.73 | 2001 |
| Nonstandard Analysis in ACL2 | 17 | 1.39 | 2001 |
| A mechanically checked proof of the AMD5K86TM floating-point division program | 41 | 2.78 | 1998 |
| ACL2 Theorems About Commercial Microprocessors | 58 | 6.34 | 1996 |
| Functional instantiation in first-order logic | 31 | 3.85 | 1991 |
