| Fares Fraij and Steve Roach. Proof of Transitive Closure Property of Directed Acyclic Graphs |
| Rex Page. Computational Logic in the Undergraduate Curriculum |
| John Cowles and Ruben Gamboa. \triangle = \square |
| J Moore. Automatically Computing Functional Instantiations |
| Laurence Pierre, Renaud Clavel and Regis Leveugle. ACL2 for the Verification of Fault-Tolerance Properties: First Results |
| Matt Kaufmann, Jacob Kornerup and Mark Reitblatt. Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover |
| Ryan Ralston. ACL2-Certified AVL Trees |
| Freek Verbeek and julien schmaltz. Formal Validation of Deadlock Prevention in Networks-on-Chips |
| Tom van den Broek and julien schmaltz. A Generic Implementation Model for the Formal Verification of Networks-on-Chips |
| Antonio Garcia-Dominguez, Francisco Palomo-Lozano and Inmaculada Medina-Bulo. Hypertext Navigation of ACL2 Proofs with XMLEye |
| David Greve. Automated Reasoning With Quantified Formulae |
| David Greve. Assuming Termination |
| Robert Sumners. User Control and Direction of a More Efficient Simplifier in ACL2 |
| David Rager. An Executable Model for Security Protocol JFKr |
| Robert S. Boyer and Warren A. Hunt, Jr.. Symbolic Simulation in ACL2 |
| Ruben Gamboa and John Cowles. Inverse Functions in ACL2(r) |
| Matt Kaufmann. Abbreviated Output for Input in ACL2 |
| Hanbing Liu. Proving A Specific Type Of Inequality Theorems in ACL2: a bind-free experience report |
| David Hardin and Samuel Hardin. Efficient, Formally VeriŽable Data Structures using ACL2 Single-Threaded Objects for High-Assurance Systems |
| Carl Eastlund. DoubleCheck Your Theorems |
| Carl Eastlund and Matthias Felleisen. Automatically Verified GUI Programs |