| 2017 | CADE | Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. | J Strother Moore, Marijn J. H. Heule |
| 2015 | ATVA | Machines Reasoning About Machines: 2015. | J Strother Moore |
| 2014 | ITP | Rough Diamond: An Extension of Equivalence-Based Rewriting. | Matt Kaufmann, J Strother Moore |
| 2014 | ITP | Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete. | J Strother Moore |
| 2012 | POPL | Meta-level features in an industrial-strength theorem prover. | J Strother Moore |
| 2011 | FMCAD | The role of human creativity in mechanized verification: | J Strother Moore |
| 2010 | LICS | Theorem Proving for Verification: The Early Days. | J Strother Moore |
| 2008 | SIGCSE | An open dialogue concerning the state of education policy in computer science. | Robert B. Schnabel, Duncan A. Buell, Joanna Goode, J Strother Moore, Chris Stephenson |
| 2007 | ICSE | ACL2s: "The ACL2 Sedan". | Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore |
| 2006 | LPAR | Verification Condition Generation Via Theorem Proving. | John Matthews, J Strother Moore, Sandip Ray, Daron Vroon |
| 2004 | FMCAD | Proof Styles in Operational Semantics. | Sandip Ray, J Strother Moore |
| 2004 | ICFEM | On the Adoption of Formal Methods by Industry: The ACL2 Experience. | J Strother Moore |
| 2002 | ICFP | Functional formal methods. | J Strother Moore |
| 2002 | PADL | Single-Threaded Objects in ACL2. | Robert S. Boyer, J Strother Moore |
| 2001 | CAV | Rewriting for Symbolic Execution of State Machine Models. | J Strother Moore |
| 1998 | CAV | An ACL2 Proof of Write Invalidate Cache Coherence. | J Strother Moore |
| 1998 | FMCAD | Symbolic Simulation: An ACL2 Approach. | J Strother Moore |
| 1996 | FMCAD | ACL2 Theorems About Commercial Microprocessors. | Bishop Brock, Matt Kaufmann, J Strother Moore |
| 1990 | CADE | A Theorem Prover for a Computational Logic. | Robert S. Boyer, J Strother Moore |
| 1986 | CADE | Overview of a Theorem-Prover for A Computational Logic. | Robert S. Boyer, J Strother Moore |
| 1977 | IJCAI | A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. | Robert S. Boyer, J Strother Moore |
| 1976 | POPL | Primitive Recursive Program Transformations. | Robert S. Boyer, J Strother Moore, Robert E. Shostak |
| 1973 | IJCAI | Proving Theorems about LISP Functions. | Robert S. Boyer, J Strother Moore |