J. Strother Moore

Matt Kaufmann, J. Strother Moore: Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1. ACL2 2013: 5-12

J. Strother Moore: Meta-level features in an industrial-strength theorem prover. POPL 2012: 425-426

Alan Bundy, Dieter Hutter, Cliff B. Jones, J. Strother Moore: AI meets Formal Software Development (Dagstuhl Seminar 12271). Dagstuhl Reports 2(7): 1-29 (2012)

J. Strother Moore: The role of human creativity in mechanized verification: invited talk. FMCAD 2011: 18

J. Strother Moore: Reasoning about digital artifacts with ACL2. PLPV 2011: 1-2

Matt Kaufmann, J. Strother Moore: How Can I Do That with ACL2? Recent Enhancements to ACL2. ACL2 2011: 46-60

J. Strother Moore: Theorem Proving for Verification: The Early Days. LICS 2010: 283

Matt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber: Integrating external deduction tools with ACL2. J. Applied Logic 7(1): 3-25 (2009)

Sandip Ray, Warren A. Hunt Jr., John Matthews, J. Strother Moore: A Mechanical Analysis of Program Verification Strategies. J. Autom. Reasoning 40(4): 245-269 (2008)

Bishop Brock, Matt Kaufmann, J. Strother Moore: Rewriting with Equivalence Relations in ACL2. J. Autom. Reasoning 40(4): 293-306 (2008)

David A. Greve, Matt Kaufmann, Panagiotis Manolios, J. Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1): 15-46 (2008)

Robert Schnabel, Duncan A. Buell, Joanna Goode, J. Strother Moore, Chris Stephenson: An open dialogue concerning the state of education policy in computer science. SIGCSE 2008: 114-115

Matt Kaufmann, J. Strother Moore: An ACL2 Tutorial. TPHOLs 2008: 17-21

Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore: ACL2s: "The ACL2 Sedan". Electr. Notes Theor. Comput. Sci. 174(2): 3-18 (2007)

Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore: ACL2s: "The ACL2 Sedan". ICSE Companion 2007: 59-60

J. Strother Moore: Inductive assertions and operational semantics. STTT 8(4-5): 359-371 (2006)

Matt Kaufmann, J. Strother Moore: Double rewriting for equivalential reasoning in ACL2. ACL2 2006: 103-106

John Matthews, J. Strother Moore, Sandip Ray, Daron Vroon: Verification Condition Generation Via Theorem Proving. LPAR 2006: 362-376

Hanbing Liu, J. Strother Moore: Executable JVM model for analytical reasoning: A study. Sci. Comput. Program. 57(3): 253-274 (2005)

Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith: Meta Reasoning in ACL2. TPHOLs 2005: 163-178

J. Strother Moore, Qiang Zhang: Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. TPHOLs 2005: 373-384

J. Strother Moore: A Mechanized Program Verifier. VSTTE 2005: 268-276

Sandip Ray, J. Strother Moore: Proof Styles in Operational Semantics. FMCAD 2004: 67-81

J. Strother Moore: On the Adoption of Formal Methods by Industry: The ACL2 Experience. ICFEM 2004: 13

Hanbing Liu, J. Strother Moore: Java Program Verification via a JVM Deep Embedding in ACL2. TPHOLs 2004: 184-200

Panagiotis Manolios, J. Strother Moore: Partial Functions in ACL2. J. Autom. Reasoning 31(2): 107-127 (2003)

J. Strother Moore: Inductive Assertions and Operational Semantics. CHARME 2003: 289-303

Warren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore: Linear and Nonlinear Arithmetic in ACL2. CHARME 2003: 319-333

J. Strother Moore, George Porter: The apprentice challenge. ACM Trans. Program. Lang. Syst. 24(3): 193-216 (2002)

J. Strother Moore: Functional formal methods. ICFP 2002: 123

Robert S. Boyer, J. Strother Moore: Single-Threaded Objects in ACL2. PADL 2002: 9-27

J. Strother Moore: A Grand Challenge Proposal for Formal Methods: A Verified Stack. 10th Anniversary Colloquium of UNU/IIST 2002: 161-172

Panagiotis Manolios, J. Strother Moore: On the desirability of mechanizing calculational proofs. Inf. Process. Lett. 77(2-4): 173-179 (2001)

Matt Kaufmann, J. Strother Moore: Structured Theory Development for a Mechanized Logic. J. Autom. Reasoning 26(2): 161-203 (2001)

J. Strother Moore: Rewriting for Symbolic Execution of State Machine Models. CAV 2001: 411-422

J. Strother Moore, George Porter: An Executable Formal Java Virtual Machine Thread Model. Java Virtual Machine Research and Technology Symposium 2001: 91-104

J. Strother Moore: Finite Set Theory in ACL2. TPHOLs 2001: 313-328

J. Strother Moore: A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View. Formal Methods in System Design 14(2): 213-228 (1999)

J. Strother Moore: Proving Theorems About Java-Like Byte Code. Correct System Design 1999: 139-162

Robert S. Boyer, J. Strother Moore: A computational logic handbook (2. ed.). Academic Press international series in formal methods, Academic Press 1998, isbn 978-0-12-122955-9, pp. I-XXV, 1-518

J. Strother Moore, Thomas W. Lynch, Matt Kaufmann: A Mechanically Checked Proof of the AMD5_K86^TM Floating Point Division Program. IEEE Trans. Computers 47(9): 913-926 (1998)

J. Strother Moore: An ACL2 Proof of Write Invalidate Cache Coherence. CAV 1998: 29-38

J. Strother Moore: Symbolic Simulation: An ACL2 Approach. FMCAD 1998: 334-350

Matt Kaufmann, J. Strother Moore: An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. 23(4): 203-213 (1997)

Bishop Brock, Matt Kaufmann, J. Strother Moore: ACL2 Theorems About Commercial Microprocessors. FMCAD 1996: 275-293

J. Strother Moore: A Formal Model of Asynchronous Communication and its Use in Mechanically Verifying a Biphase Mark Protocol. Formal Asp. Comput. 6(1): 60-91 (1994)

J. Strother Moore: Introduction to the OBDD Algorithm for the ATP Community. J. Autom. Reasoning 12(1): 33-46 (1994)

Robert S. Boyer, J. Strother Moore: MJRTY: A Fast Majority Vote Algorithm. Automated Reasoning: Essays in Honor of Woody Bledsoe 1991: 105-118

Robert S. Boyer, J. Strother Moore: A Theorem Prover for a Computational Logic. CADE 1990: 1-15

William R. Bevier, Warren A. Hunt Jr., J. Strother Moore, William D. Young: An Approach to Systems Verification. J. Autom. Reasoning 5(4): 411-428 (1989)

J. Strother Moore: A Mechanically Verified Language Implementation. J. Autom. Reasoning 5(4): 461-492 (1989)

Robert S. Boyer, J. Strother Moore: The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. J. Autom. Reasoning 4(2): 117-172 (1988)

Robert S. Boyer, J. Strother Moore: Overview of a Theorem-Prover for A Computational Logic. CADE 1986: 675-678

Robert S. Boyer, J. Strother Moore: Program Verification. J. Autom. Reasoning 1(1): 17-23 (1985)

Robert S. Boyer, J. Strother Moore: A Mechanical Proof of the Unsolvability of the Halting Problem. J. ACM 31(3): 441-458 (1984)

Robert S. Boyer, J. Strother Moore: A computational logic. ACM monograph series, Academic Press 1980, isbn 978-0-12-122950-4, pp. I-XIV, 1-397

J. Strother Moore: A Mechanical Proof of the Termination of Takeuchi's Function. Inf. Process. Lett. 9(4): 176-181 (1979)

Robert S. Boyer, J. Strother Moore: A Fast String Searching Algorithm. Commun. ACM 20(10): 762-772 (1977)

Robert S. Boyer, J. Strother Moore: A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. IJCAI 1977: 511-519

Robert S. Boyer, J. Strother Moore, Robert E. Shostak: Primitive Recursive Program Transformations. POPL 1976: 171-174

Robert S. Boyer, J. Strother Moore: Proving Theorems about LISP Functions. J. ACM 22(1): 129-144 (1975)

J. Strother Moore: Introducing Iteration into the Pure Lisp Theorem Prover. IEEE Trans. Software Eng. 1(3): 328-338 (1975)

Robert S. Boyer, J. Strother Moore: Proving Theorems about LISP Functions. IJCAI 1973: 486-493