Publications
This list is divided into
Talks,
Books,
Articles, and
Other.
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.
This link contains some introductory resources for learning how to use the
ACL2 theorem proving system.
The PDF versions of some of these talks were produced using ps2pdf and are not
always formatted as nicely as the Postscript versions.
 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 ``BoyerMoore 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 BoyerMoore 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)]
 ComputerAided Reasoning: An Approach, with Matt Kaufmann and
Panagiotis Manolios, Kluwer Academic Publishers, 2000. *
 ComputerAided 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 AssemblyLevel
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.
 Milestones from The Pure Lisp Theorem Prover to ACL2,
Draft submitted for publication, March, 2019.
 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. 4245.,
2017.
 Limited SecondOrder Functionality in a FirstOrder Setting, with M. Kaufmann, 2017 (submitted for publication).

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 submitted draft of this
paper is
available here.
Researchers wishing to obtain a copy of the published paper for
noncommercial private use should contact moore@cs.utexas.edu.)
 Computing Verified Machine Address Bounds during Symbolic Exploration of Code,
Provably Correct Systems, (J. Bowen, H. Langmaack and E.R. Olderog,
Eds), Springer, pp. 151172, 2017.
 Machines Reasoning About Machines: 2015,
in Automated Technology for Verification and Analysis, (B. Finkbeiner, G. Pu, and L. Zhang, Eds),
LNCS 9364, pp. 413. (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. 93109, 2015.
 WellFormedness 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 EquivalenceBased 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. 537542, 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. 406420, 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 BoyerMoore 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 267284, 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 BoyerMoore
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. 293306, May, 2008.
 A Mechanized Program Verifier, Verified Software: Theories, Tools, Experiments,
(B. Meyer and J. Woodcock, editors), Springer LNCS 4171, pp. 268276, 2008
 String Searching over Small Alphabets,
with M. Sustik, TR0762, 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. 6468, 2006.
 Integrating External
Deduction Tools with ACL2. with M. Kaufmann, S. Ray, and E. Reeber,
Journal of Applied Logic, 7(1), pp. 325, 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. 726, 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. RuizReina, R. Sumners, D. Vroon,
and M. Wilding, Journal of Functional Programming, 18(01), pp 1546, 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. 373384, 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. 163178, 2005.

Proof Styles in Operational Semantics, with S. Ray, Formal Methods in
ComputerAided Design (FMCAD 2004), A. J. Hu and A. K. Martin (eds.),
Springer Lecture Notes in Computer Science, 3312, pages 6781,
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. 184200, 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. 181196, 2004.
 Interactive
Symbolic Visualization of Semiautomatic Theorem Proving, with C. Bajaj,
S. Khandelwal, and V. Siddavanahalli, Technical Report TR0337, 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. 289303, 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. 319333, 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.), SpringerVerlag, 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 227290, 2003.
 A Computational Logic for Applicative Common LISP, with
M. Kaufmann, in A Companion to Philosophical Logic,
D. Jacquette (ed), Blackwell Publishers, pp. 724741, 2002.
 On the desirability of mechanizing calculational proofs, with P. Manolios,
Information Processing Letters, 77 (24), February, 2001,
pp. 173179.
 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. 107127, 2003.
 Finite Set Theory in ACL2,
Theorem Proving for Higher Order Logics  TPHOLs '01,
R. J. Boulton and P. B. Jackson (eds.), SpringerVerlag LNCS 2152,
pp 313328, Sep 2001.
 Rewriting for Symbolic Execution of State
Machine Models, Proceedings of CAV 01,
G. Berry, H. COmon, and A. Finkel (eds.), SpringerVerlag LNCS 2102,
pp 411422, 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. 124, May, 2002.

Towards a Mechanically Checked Theory of Computation: A Progress
Report, in J. Minker, ed., Logic and Artificial Intelligence,
pp. 549575, Kluwer, 2000.
 SingleThreaded Objects in ACL2,
with R. Boyer, in
S. Krishnamurthi and C. R. Ramakrishnan (eds.),
PADL 2002, LNCS 2257, pp. 927, 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. 141175, 2005.
(ACL2 Script)
 Structured Theory Development for a Mechanized Logic,
with M. Kaufmann, Journal of Automated Reasoning, 26(2),
pp. 161203, 2001.
 Proving Theorems about Javalike Byte Code,
in E.R. Olderog and B. Steffen (eds.) Correct System Design  Recent
Insights and Advances, LNCS 1710, pp. 139162, 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 ComputerAided Design (FMCAD'98), SpringerVerlag LNCS 1522,
pp. 334350, 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, SpringerVerlag LNCS 1427,
pp. 2938, 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. 213228.
(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
includebook
to
load it into your ACL2 and then do (inpackage "SMALLMACHINE")
.)
 A
Mechanically Checked Proof of the Correctness of the Kernel of the AMD5k86
FloatingPoint Division Program, with T. Lynch and M. Kaufmann, IEEE
Transactions on Computers, 47(9), pp. 913926, 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 ComputerAided Design (FMCAD'96),
SpringerVerlag, pp. 275293, 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. 203213. *
 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. 6091. *
 Introduction to the OBDD Algorithm for the ATP
Community. In Journal of Automated Reasoning, Kluwer Academic
Publishers, 6(1), 1994, pp. 3345.
[benchmarks].
 The BoyerMoore
Theorem Prover and Its Interactive Enhancement, with M. Kaufmann and
R. S. Boyer, Computers and Mathematics with Applications,
29(2), 1995, pp. 2762. *
 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. 726.
 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. 105117. *
 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, SpringerVerlag Texts and Monographs in Computer Science,
1990, pp. 5466.
 A
Theorem Prover for a Computational Logic, with R. S. Boyer,
keynote address, Automated Deduction  CADE10, Lecture Notes
in Computer Science 449, SpringerVerlag, 1990, pp. 115.
 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. 461492.
 A Mechanically Verified Language
Implementation. In Journal of Automated Reasoning, Kluwer Academic
Publishers, 5(4), 1989, pp. 461492.
 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. 117172.
 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. 83124.
(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. 1723.
 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. 133168.
 ProofChecking, TheoremProving, 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. 119132.
 Proof
Checking the RSA Public Key Encryption Algorithm, with
R. S. Boyer. American Mathematical Monthly, 91(3), March
1984, pp. 181189.
 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. 441458.
 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 TheoremProver for Recursive Functions, with R.S. Boyer. Software
Engineering Notes, Association for Computing Machinery, 5(3),
1980, pp. 2627.
 The FORTRAN Verification System, with R. S. Boyer. Software
Engineering Notes, Association for Computing Machinery, 5(3),
1980, pp. 1617.
 A Statement of Position. Software Engineering Notes, Association
for Computing Machinery, 5(3), 1980, pp 2324.
 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 252253.
 A Mechanical Proof of the Termination of Takeuchi's
Function. Information Processing Letters, 9(4), 1979,
pp. 176181.
 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. 511519.
 A Fast String Searching Algorithm, with R.S. Boyer. Communications of
the Association for Computing Machinery, 20(10), 1977,
pp. 762772. * (Here is a large (1.1MB) pdf image of
the paper.)
 Introducing Iteration into the Pure LISP TheoremProver. IEEE
Transactions on Software Engineering, 1(3), 1975, pp. 328338.
(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. 1314.
 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.129144. (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.486493.)*
 The Sharing of Structure in Theoremproving Programs, with R.S. Boyer.
In B. Meltzer and D. Michie (eds), Machine Intelligence 7. Edinburgh
University Press, 1972, pp. 101116.
 Automation of Mathematical Induction
as part of the History of Logic (1.25MB pdf), with C. P. Wirth,
unpublished, pp. 1108, January, 2014.
 Final
Report of the Gender Equity Task Force (11MB pdf), Provost's Task Force
on Faculty Gender Equity, J Strother Moore and Gretchen Ritter (cochairs),
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 1014, 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. 1618.

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
8Bit Parallel IO Byzantine Agreement Processor. NASA CR189588, 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 CSL812,
Xerox Palo Alto Research Center, 1981.*
 A TheoremProver for Recursive Functions: A User's
Manual, with R.S. Boyer. Technical Report CSL91, 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. 8997.
 On Why It Is Impossible to Prove that
the BDX930 Dispatcher Implements a TimeSharing System, with
R.S. Boyer. Sections 14 and 15 of Investigation, Development, and
Evaluation of Performance Proving for FaultTolerant Computer Final Report,
covering the period September 1978 to June 1982, P.M. MelliarSmith,
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. 511519.
 The INTERLISP Virtual Machine
Specification. Technical Report CSL765, 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 77Editor, 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.