Publications

Those entries marked * are my favorite papers. For each such paper I have a short note explaining the basic idea, or, in the case of the two theorem provers (NQTHM and ACL2), giving a quick overview of the entire body work on the subject. You may click on the * to see the related note.

You may return to my home page here.

About ACL2

Talks

• Industrial Hardware and Software Verification with ACL2, with Warren A. Hunt, Matt Kaufmann, and Anna Slobodova, delivered at the Royal Society, London, April, 2016. (See the Article by the same name below for the paper.)
• Machines Reasoning about Machines -- 2015 My standard introduction to ACL2, sketching the applications of the various ``Boyer-Moore provers'' to industrially interesting projects from the beginning through the Fall, 2015.
• The Role of Human Creativity in Mechanized Verification, FMCAD 2011 Keynote. Mechanized formal methods aims to automate much of creativity involved in produced mechanically verified artifacts. This talk argues that the tendency to polish our creations -- in engineering, art, or mathematics -- hides the creative process and thus obscures the very thing we, as researchers, should be investigating.
• Theorem Proving for Verification -- the Early Days An informal history of the first 10 years of the Boyer-Moore theorem prover, delivered as a keynote talk at FLoC 2010, Edinburgh, July, 2010.
• Mechanized Operational Semantics five lectures on mechanized operational semantics delivered at the Marktoberdorf 2008 Summer School.
• Automated Reasoning and The ACL2 Theorem Proving System by J Strother Moore and Matt Kaufmann, delivered at the 2006 Visions of Computing Lecture, Department of Computer Sciences, University of Texas at Austin, November 9, 2006, in celebration of the 2005 ACM Software System Award.
• A Mechanized Program Verifier
  by J Strother Moore, delivered at the Verification Grand Challenge Workshop, Zurich, October 12, 2005.
  [a small html file]
• ACL2: A Program Verifier for Applicative Common Lisp
  by Matt Kaufmann and J Strother Moore, delivered at the International Lisp Conference 2005, Stanford, CA, June 21, 2005.
  [PDF 150 KB]
• The ACL2 Project
  -- some remarks made at SRI, Feb 21, 2005.
  [PDF 76 KB]
• Finite Set Theory in ACL2
  -- presented at TPHOLs 2001, Edinburgh, September, 2001.
  [Postscript (0.27MB)] [PDF (0.31MB)]
  
• Rewriting for Symbolic Execution of State Machine Models
  -- presented at CAV'01, Paris, July, 2001.
  [Postscript (0.30MB)] [PDF (0.30MB)]
  
• Formal Methods: Practice and Pedagogy
  -- presented at JENUI 03, Cadiz, Spain, July, 2003.
  [Postscript (1.25MB)] [PDF (0.80MB)] [ACL2 log file of demo (0.10MB)]
  
• Inductive Assertions and Operational Semantics
  -- presented at CHARME 03, L'Aquila, Italy and Dagstuhl, Germany Oct/Nov 03.
  [Postscript (0.30MB)] [PDF (0.40MB)]
  
• Memory Taggings and Dynamic Data Structures
  -- presented at the ACL2 Workshop 2003, Boulder, Colorado, July, 2003.
  [Postscript (0.195MB)] [PDF (0.240MB)]
  

Books

• Computer-Aided Reasoning: An Approach, with Matt Kaufmann and Panagiotis Manolios, Kluwer Academic Publishers, 2000. *
• Computer-Aided Reasoning: ACL2 Case Studies, Editor, with Matt Kaufmann and Panagiotis Manolios, Kluwer Academic Publishers, 2000. *
• A Computational Logic Handbook, with R.S. Boyer. Academic Press, London, 1997. Second Edition.
• Piton:  A Mechanically Verified Assembly-Level Language, J Strother Moore, Automated Reasoning Series, Kluwer Academic Publishers, 1996. *
• Journal of Automated Reasoning, Special Issue on System Verification, J Strother Moore, Editor, Vol. 5 No. 4 1989.
• A Computational Logic Handbook, with R.S. Boyer. Academic Press, New York, 1988.
• A Computational Logic, with R.S. Boyer. Academic Press, New York, 1979. *
• The Correctness Problem in Computer Science Editor, with R.S. Boyer. Academic Press, London, 1981.

Articles

• ACL2 Support for Floating-Point Computations, with M. Kaufmann, The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part I (Cavalcanti, A. and Baxter, J., Eds), Springer Nature Switzerland, Cham, pp 251-207, DOI https://doi.org/10.1007/978-3-031-66676-6_13, 2024.
• Recollections of Hope Park Square, 1970 — 1973, Mathematical Reasoning: The History and Impact of the DReaM Group (Michaelson, G., Eds), Springer, Cham, Switzerland, pp. 37-49, DOI https://doi.org/10.1007/978-3-030-77879-8, 2021.
• VWSIM: A Circuit Simulator, with W. A. Hunt and V. Ramanathan, Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2022) (R. Summers and C. Chau, Eds), Electronic Proceedings in Theoretical Computer Science, 359, pp. 61–75, DOI http://dx.doi.org/10.4204/EPTCS.359.7, May, 2022.
• Milestones from The Pure Lisp Theorem Prover to ACL2, Formal Aspects of Computing, Springer, DOI https://doi.org/10.1007/s00165-019-00490-3, 2019.
• Limited Second-Order Functionality in a First-Order Setting, with M. Kaufmann, Journal of Automated Reasoning, Springer, DOI https://doi.org/10.1007/s10817-018-09505-9, 2018.
• Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions, with M. Heule, . ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, (G. Reger and D. Traytel, Eds), 51, pp. 42-45., 2017.
• Industrial Hardware and Software Verification with ACL2, with W. A. Hunt, Jr., M. Kaufmann and A. Slobodova, Verified Trustworthy Software Systems, (P. Gardner, P. O'Hearn, M. Gordon, G. Morrisett and F. B. Schneider, Eds), Philosophical Transactions A, Royal Society Publishing, 374, DOI 10.1098/rsta.2015.0399, September, 2017. (A copy of the paper is also available from the NIH website.)
• Computing Verified Machine Address Bounds during Symbolic Exploration of Code, Provably Correct Systems, (J. Bowen, H. Langmaack and E.-R. Olderog, Eds), Springer, pp. 151-172, 2017.
• Automation of Mathematical Induction as part of the History of Logic, with C-P Wirth, IfCoLog Journal of Logics and their Applications4(5), pp. 1505-1634, 2017.
• Machines Reasoning About Machines: 2015, in Automated Technology for Verification and Analysis, (B. Finkbeiner, G. Pu, and L. Zhang, Eds), LNCS 9364, pp. 4-13. (Slides available here.)
• Stateman: Using Metafunctions to Manage Large Terms Representing Machine States, in Proceedings of the 13th International Workshop on the ACL2 Theorem Prover, (M. Kaufmann and D. Rager, Eds.), EPTCS, 192, pp. 93-109, 2015.
• Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors, with M. Kaufmann, in Proceedings of the International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS) 2015, (M. K. Ganai and C. Wang, Eds.), Austin, TX, Oct, 2015.
• Rough Diamond: An Extension of Equivalence-Based Rewriting, with M. Kaufmann, in Proceedings of ITP 2014: 5th International Conference on Interactive Theorem Proving, (G. Klein and R. Gamboa, Eds.), LNAI 8558, pp. 537-542, 2014. (Draft)
• Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete", in Proceedings of ITP 2014: 5th International Conference on Interactive Theorem Proving, (G. Klein and R. Gamboa, Eds.), LNAI 8558, pp. 406-420, 2014. (Draft)
• Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4, with M. Kaufmann, Proceedings of the Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, (F. Verbeek and J. Schmaltz, Eds.), EPTCS 152, 2014.
• How Can I Do That with ACL2? Recent Enhancements to ACL2, with M. Kaufmann. ACL2 Workshop, 2011, Austin, TX, Nov, 2011.
• Automatically Computing Functional Instantiations, in Proceedings of the ACL2 Workshop 2009(eds. D. Russinoff and S. Ray), Boston, 2009.
• A Mechanically Checked Proof of the Correctness of the Boyer-Moore Fast String Searching Algorithm, with M. Martinez, in Proceedings of Marktoberdorf Summer School, 2008: Engineering Methods and Tools for Software Safety and Security, M. Broy, W. Sitou, and T. Hoare (eds), IOS Press, pp 267-284, 2009. (In a related piece of work, see the unpublished Honors Thesis by Erik Toibazarov, An ACL2 Proof of the Correctness of the Preprocessing for a Variant of the Boyer-Moore Fast String Searching Algorithm, UTCS April, 2013.)
• An ACL2 Tutorial, with M. Kaufmann, Proceedings of Theorem Proving on Higher Order Logics, Lecture Notes in Computer Science, 5170, Springer Berlin, Heidelberg, 2008.
• Rewriting with Equivalence Relations in ACL2, with B. Brock and M. Kaufmann, Journal of Automated Reasoning, 40(4), pp. 293-306, May, 2008.
• A Mechanized Program Verifier, Verified Software: Theories, Tools, Experiments, (B. Meyer and J. Woodcock, editors), Springer LNCS 4171, pp. 268-276, 2008
• String Searching over Small Alphabets, with M. Sustik, TR-07-62, Department of Computer Sciences, University of Texas at Austin, December, 2007.
• Integrating CCG Analysis into ACL2, with M. Kaufmann, P. Manolios, and D. Vroon, Proceedings of the Eighth International Workshop on Termination (part of FLoC 2006), pp. 64--68, 2006.
• Integrating External Deduction Tools with ACL2. with M. Kaufmann, S. Ray, and E. Reeber, Journal of Applied Logic, 7(1), pp. 3-25, March, 2009. (Preliminary version appeared in Proceedings of the 6th International Workshop on the Implementation of Logics (IWIL 2006) (C. Benzmueller, B. Fischer, and G. Sutcliffe, editors), CEUR Workshop Proceedings Vol. 212, Phnom Penh, Cambodia, pp. 7-26, November 2006.)
• A Mechanical Analysis of Program Verification Strategies, with S. Ray, W. Hunt, and J. Matthews, Journal of Automated Reasoning, March, 2008.
• Maintaining the ACL2 Theorem Proving System, with M. Kaufmann. Invited talk. Proceedings of the FLoC'06 Workshop on Empirically Successful Computerized Reasoning, 3rd International Joint Conference on Automated Reasoning, (G. Sutcliffe, R. Schmidt, and S. Schulz, eds.), CEUR Workshop Proceedings, 192, Seattle, August, 2006.
• Verification Condition Generation via Theorem Proving, with J. Matthews, S. Ray, and D. Vroon, Proceedings of the 13th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR 2006), M. Hermann and A. Voronkov (eds.), Springer, November, 2006.
• Efficient Execution in an Automated Reasoning Environment, with D. A. Greve, M. Kaufmann, P. Manolios, S. Ray, J. L. Ruiz-Reina, R. Sumners, D. Vroon, and M. Wilding, Journal of Functional Programming, 18(01), pp 15-46, January, 2008.
• Double Rewriting for Equivalential Reasoning in ACL2, with M. Kaufmann Proceedings of the ACL2 Workshop 2006, ACM Digital Library (to appear).
• Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2, with Q. Zhang, 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 373-384, 2005.
• Meta Reasoning in ACL2, with W. A. Hunt and M. Kaufmann and R. B. Krug and E. W. Smith, 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer Lecture Notes in Computer Science, 3603, pp. 163--178, 2005.
• Proof Styles in Operational Semantics, with S. Ray, Formal Methods in Computer-Aided Design (FMCAD 2004), A. J. Hu and A. K. Martin (eds.), Springer Lecture Notes in Computer Science, 3312, pages 67-81, 2004.
• Java Program Verification via a JVM Deep Embedding in ACL2, with H. Liu, TPHOLS 2004, K. Slind, A. Bunker, and G. Gopalakrishnan (eds), Springer Lecture Notes in Computer Science, 3223, pp. 184-200, 2004.
• Some Key Research Problems in Automated Theorem Proving for Hardware and Software Verification, with M. Kaufmann, Spanish Royal Academy of Science (RACSAM), 98(1), pp. 181-196, 2004.
• Interactive Symbolic Visualization of Semi-automatic Theorem Proving, with C. Bajaj, S. Khandelwal, and V. Siddavanahalli, Technical Report TR-03-37, Department of Computer Sciences, University of Texas at Austin, August 2003. (Short version, presented as in interactive poster at IEEE Symposium on Information Visualization 2003. Seattle, WA.
• Executable JVM Model for Analytical Reasoning: A Study, with H. Liu, ACM SIGPLAN 2003 Workshop on Interpreters, Virtual Machines and Emulators, San Diego, CA, June 12, 2003.
• Inductive Assertions and Operational Semantics, CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 289-303, 2003.
• Linear and Nonlinear Arithmetic in ACL2, with W. A. Hunt and R. B. Krug, CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 319-333, 2003.
• Memory Taggings and Dynamic Data Structures, ACL2 Workshop 2003, M. Kaufmann, W. A. Hunt, Jr., and J S. Moore (eds.), Boulder, Co., July, 2003.
• Model Language for Patent and Licensing Agreements for Industrially Sponsored University Research In Information Technology, CRA Chairs Conference, Snowbird, Utah, July, 2002. (pdf version; MS Word version). This document became the basis of Computer Research Association (CRA) Best Practices memo.
• A Grand Challenge Proposal for Formal Methods: A Verified Stack, presented at 10th Anniversary Colloquium of the UN University International Institute for Software Technology: Formal Methods at the Crossroads, Lisbon, Portugal, March, 2002. (To appear in Formal Methods at the Crossroads: from Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, B. K. Aichernig and T. Maibaum (eds.), Springer-Verlag, 2003).
• Proving Theorems about Java and the JVM with ACL2, Models, Algebras and Logic of Engineering Software, M. Broy and M. Pizka (eds), IOS Press, Amsterdam, pp 227-290, 2003.
• A Computational Logic for Applicative Common LISP, with M. Kaufmann, in A Companion to Philosophical Logic, D. Jacquette (ed), Blackwell Publishers, pp. 724-741, 2002.
• On the desirability of mechanizing calculational proofs, with P. Manolios, Information Processing Letters, 77 (2-4), February, 2001, pp. 173-179.
• Formal Models of Java at the JVM Level -- A Survey from the ACL2 Perspective, with R. Krug, H. Liu, and G. Porter, Workshop on Formal Techniques for Java Programs, in association with ECOOP 2001, June, 2001 (long version).
• Partial Functions in ACL2, with Panagiotis Manolios, Journal of Automated Reasoning, Kluwer, 31(2), pp. 107-127, 2003.
• Finite Set Theory in ACL2, Theorem Proving for Higher Order Logics -- TPHOLs '01, R. J. Boulton and P. B. Jackson (eds.), Springer-Verlag LNCS 2152, pp 313-328, Sep 2001.
• Rewriting for Symbolic Execution of State Machine Models, Proceedings of CAV 01, G. Berry, H. COmon, and A. Finkel (eds.), Springer-Verlag LNCS 2102, pp 411-422, July, 2001.
• An Executable Formal Java Virtual Machine Thread Model, with G. Porter, in Java Virtual Machine Research and Technology Symposium (JVM '01), USENIX, April, 2001.
• The Apprentice Challenge, with G. Porter, ACM TOPLAS 24(3), pp. 1--24, May, 2002.
• Towards a Mechanically Checked Theory of Computation: A Progress Report, in J. Minker, ed., Logic and Artificial Intelligence, pp. 549--575, Kluwer, 2000.
• Single-Threaded Objects in ACL2, with R. Boyer, in S. Krishnamurthi and C. R. Ramakrishnan (eds.), PADL 2002, LNCS 2257, pp. 9--27, 2002.
• A Mechanically Checked Proof of a Comparator Sort Algorithm, with B. Brock, in M. Broy, J. Gruenbauer, D. Harel, and C. A. R. Hoare (eds.) Engineering Theories of Software Intensive Systems, Springer NATO Science Series II, 195, pp. 141-175, 2005. (ACL2 Script)
• Structured Theory Development for a Mechanized Logic, with M. Kaufmann, Journal of Automated Reasoning, 26(2), pp. 161-203, 2001.
• Proving Theorems about Java-like Byte Code, in E.-R. Olderog and B. Steffen (eds.) Correct System Design -- Recent Insights and Advances, LNCS 1710, pp. 139-162, 1999. (ACL2 Script)
• Symbolic Simulation: An ACL2 Approach, in G. Gopalakrishnan and P. Windley (eds.) Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD'98), Springer-Verlag LNCS 1522, pp. 334-350, November, 1998. (ACL2 Script)
• An ACL2 Proof of Write Invalidate Cache Coherence, in A. J. Hu and M. Y. Vardi (eds.) Computed Aided Verification: 10th International Conference, CAV '98, Springer-Verlag LNCS 1427, pp. 29-38, 1998. (ACL2 Scripts)
• A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View. Formal Methods in System Design, 14(2), March, 1999, pp. 213-228. (ACL2 script).
• Mechanized Formal Reasoning about Programs and Computing Machines, with R. S. Boyer, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos , MIT Press, 1996. (ACL2 Script: After fetching this script, use include-book to load it into your ACL2 and then do (in-package "SMALL-MACHINE").)
• A Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86 Floating-Point Division Program, with T. Lynch and M. Kaufmann, IEEE Transactions on Computers, 47(9), pp. 913-926, Sep., 1998. * [The URL provided is an early draft of the paper eventually published.]
• ACL2 Theorems about Commercial Microprocessors with B. Brock and M. Kaufmann. In M. Srivas and A. Camilleri (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275-293, 1996. *
• An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, with M. Kaufmann, IEEE Transactions on Software Engineering 23(4), April 1997, pp. 203-213. *
• A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol. In Formal Aspects of Computing, 6(1) 1994, pp. 60-91. *
• Introduction to the OBDD Algorithm for the ATP Community. In Journal of Automated Reasoning, Kluwer Academic Publishers, 6(1), 1994, pp. 33-45. [benchmarks].
• The Boyer-Moore Theorem Prover and Its Interactive Enhancement, with M. Kaufmann and R. S. Boyer, Computers and Mathematics with Applications, 29(2), 1995, pp. 27-62. *
• Functional Instantiation in First Order Logic, with R.S. Boyer, D.M. Goldschlag, and M. Kaufmann. In V. Lifschitz (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, Academic Press, 1991, pp. 7-26.
• MJRTY - A Fast Majority Vote Algorithm, with R.S. Boyer. In R.S. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe, Automated Reasoning Series, Kluwer Academic Publishers, Dordrecht, The Netherlands, 1991, pp. 105-117. *
• The Use of a Formal Simulator to Verify a Simple Real Time Control Program, with R.S. Boyer and M.W. Green. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra (eds.), Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra, Springer-Verlag Texts and Monographs in Computer Science, 1990, pp. 54-66.
• A Theorem Prover for a Computational Logic, with R. S. Boyer, keynote address, Automated Deduction -- CADE-10, Lecture Notes in Computer Science 449, Springer-Verlag, 1990, pp. 1-15.
• Special Issue on System Verification, with W.R. Bevier, W.A. Hunt, and W.D. Young. Journal of Automated Reasoning, Kluwer Academic Publishers, 5(4), 1989, pp. 461-492.
• A Mechanically Verified Language Implementation. In Journal of Automated Reasoning, Kluwer Academic Publishers, 5(4), 1989, pp. 461-492.
• The Addition of Bounded Quantification and Partial Functions to a Computational Logic and Its Theorem Prover, with R. S. Boyer. In Journal of Automated Reasoning, Kluwer Academic Publishers, 4(2), 1988, pp. 117-172.
• Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, with R.S. Boyer. In Machine Intelligence 11, Oxford University Press, 1988, pp. 83-124. (I do not have an online copy of this paper and the book is widely unavailable. Here is a 5MB pdf file that contains a version of the paper produced by optical character scanning.)
• The Code for a Computational Logic, with R. S. Boyer, Technical Report 24, Computational Logic, Inc., Austin, Texas, 1988.
• Program Verification, with R.S. Boyer. Journal of Automated Reasoning, 1(1), 1985, pp. 17-23.
• A Mechanical Proof of the Turing Completeness of PURE LISP, with R. S. Boyer. In W. W. Bledsoe and D. W. Loveland (eds.), Contemporary Mathematics, Volume 29, Automated Theorem Proving: After 25 Years, American Mathematical Society, Providence, Rhode Island, 1984, pp. 133-168.
• Proof-Checking, Theorem-Proving, and Program Verification, with R. S. Boyer. In W. W. Bledsoe and D. W. Loveland (eds), Contemporary Mathematics, Volume 29, Automated Theorem Proving: After 25 Years, American Mathematical Society, Providence, Rhode Island, 1984, pp. 119-132.
• Proof Checking the RSA Public Key Encryption Algorithm, with R. S. Boyer. American Mathematical Monthly, 91(3), March 1984, pp. 181-189.
• A Mechanical Proof of the Unsolvability of the Halting Problem, with R. S. Boyer. Journal of the Association for Computing Machinery, 31(3), July 1984, pp. 441-458.
• A Verification Condition Generator for FORTRAN, with R.S. Boyer. In R.S. Boyer and J S. Moore (eds), The Correctness Problem in Computer Science, Academic Press, London, 1981.
• Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures, with R.S. Boyer. In R.S. Boyer and J S. Moore (eds), The Correctness Problem in Computer Science, Academic Press, London, 1981.
• A Theorem-Prover for Recursive Functions, with R.S. Boyer. Software Engineering Notes, Association for Computing Machinery, 5(3), 1980, pp. 26-27.
• The FORTRAN Verification System, with R. S. Boyer. Software Engineering Notes, Association for Computing Machinery, 5(3), 1980, pp. 16-17.
• A Statement of Position. Software Engineering Notes, Association for Computing Machinery, 5(3), 1980, pp 23-24.
• Program Verification: An Approach to Reliable Hardware and Software, with L. Lamport. Transactions of the American Nuclear Society, American Nuclear Society, Vol. 35, November, 1980, pp 252-253.
• A Mechanical Proof of the Termination of Takeuchi's Function. Information Processing Letters, 9(4), 1979, pp. 176-181.
• A Lemma Driven Automatic Theorem Prover for Recursive Function Theory, with R. S. Boyer. Proceedings of the 5th International Joint Conference on Artificial Intelligence, 1977, pp. 511-519.
• A Fast String Searching Algorithm, with R.S. Boyer. Communications of the Association for Computing Machinery, 20(10), 1977, pp. 762-772. * (Here is a large (1.1MB) pdf image of the paper.)
• Introducing Iteration into the Pure LISP Theorem-Prover. IEEE Transactions on Software Engineering, 1(3), 1975, pp. 328-338. (ocr scanned copy 3.7MB).
• Automatic Proof of the Correctness of a Binary Addition Algorithm. SIGART Newsletter, Association for Computing Machinery, No. 52, 1975, pp. 13-14.
• Primitive Recursive Program Transformation, with R. S. Boyer and R. E. Shostak. Proceedings of the Third Association for Computing Machinery Symposium on Principles of Programming Languages, Atlanta, 1976.
• Proving Theorems about LISP Functions, with R.S. Boyer. Journal of the Association for Computing Machinery, 22(1), 1975, pp.129-144. (This is a longer version of a paper by the same name presented at the 3rd International Joint Conference on Artificial Intelligence, Stanford University, 1973, pp.486-493.)*
• The Sharing of Structure in Theorem-proving Programs, with R.S. Boyer. In B. Meltzer and D. Michie (eds), Machine Intelligence 7. Edinburgh University Press, 1972, pp. 101-116.

Other

• ACL2 Induction Heuristics, December, 2020.
• Final Report of the Gender Equity Task Force (11MB pdf), Provost's Task Force on Faculty Gender Equity, J Strother Moore and Gretchen Ritter (co-chairs), University of Texas at Austin, November 3, 2008.
• A Mechanized Program Verifier (98 KB pdf) a position paper submitted to the IFIP Working Conference on the Program Verifier Challenge, Zurich, Switzerland, Oct 10--14, 2005
• A Quick and Dirty Sketch of a Toy Logic, 1998.
• A Precise Description of the ACL2 Logic, with M. Kaufmann, 1997.
• Design Goals of ACL2, with M. Kaufmann. CLI Technical Report 101, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1994.
• Metafunctions in Nqthm and Acl2, with Matt Kaufmann and R. S. Boyer, Proceedings of the Workshop on Correctness and Metatheoretic Extensibility of Automated Reasoning Systems, INRIA Lorraine, Nancy, France, 1994, pp. 16-18.
• On the Difficulty of Automating Inductive Reasoning, with J Moore, Remarks made at a workshop on inductive reasoning, Sarasota Springs, NY, June, 1992.
• The Role of Automated Reasoning in Integrated System Verification Environments, with D. I. Good and M. Kaufmann. CLI Technical Report 73, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1992.
• Should We Begin a Standardization Process for Interface Logics?, with M. Kaufmann. CLI Technical Report 72, Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1992.
• Mechanically Verified Hardware Implementing an 8-Bit Parallel IO Byzantine Agreement Processor. NASA CR-189588, 1992.
• The Mechanical Verification of a FORTRAN Square Root Program, with R. S. Boyer. Technical Report, Computer Science Laboratory, SRI International, 1981.
• Text Editing Primitives - The TXDT Package. Technical Report CSL-81-2, Xerox Palo Alto Research Center, 1981.*
• A Theorem-Prover for Recursive Functions: A User's Manual, with R.S. Boyer. Technical Report CSL-91, Computer Science Laboratory, SRI International, 1979.
• A Guided Tour Through a Working Theorem Prover. Proceedings of the Fourth Work shop on Artificial Intelligence, Institut fur Informatik, Universitat Bonn, 1979, pp. 89-97.
• On Why It Is Impossible to Prove that the BDX930 Dispatcher Implements a Time-Sharing System, with R.S. Boyer. Sections 14 and 15 of Investigation, Development, and Evaluation of Performance Proving for Fault-Tolerant Computer Final Report, covering the period September 1978 to June 1982, P.M. Melliar-Smith, K. Levitt, R. Schwartz, R. Boyer, J Moore, D. Hare, R. Shostak, M. Moriconi, M. Green, and W.D. Elliot, SRI, July 1982. (This is the first attempt by Boyer and me to formalize a commercial machine's ISA and analyze machine code in the logic of our theorem prover of the era. The report does not contain a date but we believe the work was carried out between 1978 -- the beginning of the final reporting period mentioned above -- and our departure from SRI in the summer of 1981.)
• A Lemma Driven Automatic Theorem Prover for Recursive Function Theory, with R.S. Boyer. Proceedings of the 5th International Joint Conference on Artificial Intelligence, 1977, pp. 511-519.
• The INTERLISP Virtual Machine Specification. Technical Report CSL-76-5, Xerox Palo Alto Research Center, 1976. [This is a scanned copy of the report; PARC is apparently no longer distributing them.]
• Computational Logic: Structure Sharing and Proof of Program Properties. PhD Thesis, Department of Computational Logic,University of Edinburgh, 1973. (16 MB scanned pdf) (See also the copy at the University of Edinburgh repository.) **
• The 77-Editor, with R.S. Boyer and D.J.M. Davies. Technical Report 62, Department of Computational Logic, University of Edinburgh, 1973. (The linked file was produced by OCR from a scanned copy of the manual.)
• The GSS Package. Technical Report 51, Department of Computational Logic, University of Edinburgh, 1972.