J Strother Moore

According to our database, J Strother Moore authored at least 81 papers between 1973 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Advances in ACL2 Proof Debugging Tools.

Matt Kaufmann, J Strother Moore

Proceedings of the 18th International Workshop on the ACL2 Theorem Prover and Its Applications, 2023

2022

VWSIM: A Circuit Simulator.

Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore

Proceedings of the Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications, 2022

2020

Limited Second-Order Functionality in a First-Order Setting.

Matt Kaufmann, J Strother Moore

J. Autom. Reason., 2020

Iteration in ACL2.

Matt Kaufmann, J Strother Moore

Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications, 2020

2019

Milestones from the Pure Lisp theorem prover to ACL2.

J Strother Moore

Formal Aspects Comput., 2019

2017

Automation of Mathematical Induction as part of the History of Logic.

J Strother Moore, Claus-Peter Wirth

FLAP, 2017

Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions.

J Strother Moore, Marijn J. H. Heule

Proceedings of the ARCADE 2017, 2017

Computing Verified Machine Address Bounds During Symbolic Exploration of Code.

J Strother Moore

Proceedings of the Provably Correct Systems, 2017

2015

Stateman: Using Metafunctions to Manage Large Terms Representing Machine States.

J Strother Moore

Proceedings of the Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, 2015

Machines Reasoning About Machines: 2015.

J Strother Moore

Proceedings of the Automated Technology for Verification and Analysis, 2015

2014

Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4.

Matt Kaufmann, J Strother Moore

Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete.

J Strother Moore

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Rough Diamond: An Extension of Equivalence-Based Rewriting.

Matt Kaufmann, J Strother Moore

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1

Matt Kaufmann, J Strother Moore

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

2012

AI meets Formal Software Development (Dagstuhl Seminar 12271).

Alan Bundy, Dieter Hutter, Cliff B. Jones, J Strother Moore

Dagstuhl Reports, 2012

Meta-level features in an industrial-strength theorem prover.

J Strother Moore

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

How Can I Do That with ACL2? Recent Enhancements to ACL2

Matt Kaufmann, J Strother Moore

Proceedings of the Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, 2011

Reasoning about digital artifacts with ACL2.

J Strother Moore

Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, 2011

The role of human creativity in mechanized verification: <i>invited talk</i>.

J Strother Moore

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2010

Theorem Proving for Verification: The Early Days.

J Strother Moore

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

ACL2 and Its Applications to Digital System Verification.

Matt Kaufmann, J Strother Moore

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Integrating external deduction tools with ACL2.

Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber

J. Appl. Log., 2009

2008

Efficient execution in an automated reasoning environment.

David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding

J. Funct. Program., 2008

A Mechanical Analysis of Program Verification Strategies.

Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore

J. Autom. Reason., 2008

Rewriting with Equivalence Relations in ACL2.

Bishop Brock, Matt Kaufmann, J Strother Moore

J. Autom. Reason., 2008

An ACL2 Tutorial.

Matt Kaufmann, J Strother Moore

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

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

Proceedings of the 39th SIGCSE Technical Symposium on Computer Science Education, 2008

2006

Inductive assertions and operational semantics.

J Strother Moore

Int. J. Softw. Tools Technol. Transf., 2006

ACL2s: "The ACL2 Sedan".

Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore

Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

Verification Condition Generation Via Theorem Proving.

John Matthews, J Strother Moore, Sandip Ray, Daron Vroon

Proceedings of the Logic for Programming, 2006

Double rewriting for equivalential reasoning in ACL2.

Matt Kaufmann, J Strother Moore

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, 2006

2005

Executable JVM model for analytical reasoning: A study.

Hanbing Liu, J Strother Moore

Sci. Comput. Program., 2005

A Mechanized Program Verifier.

J Strother Moore

Proceedings of the Verified Software: Theories, 2005

Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2.

J Strother Moore, Qiang Zhang

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Meta Reasoning in ACL2.

Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

2004

Java Program Verification via a JVM Deep Embedding in ACL2.

Hanbing Liu, J Strother Moore

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

On the Adoption of Formal Methods by Industry: The ACL2 Experience.

J Strother Moore

Proceedings of the Formal Methods and Software Engineering, 2004

Proof Styles in Operational Semantics.

Sandip Ray, J Strother Moore

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

2003

Partial Functions in ACL2.

Panagiotis Manolios, J Strother Moore

J. Autom. Reason., 2003

Linear and Nonlinear Arithmetic in ACL2.

Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

The apprentice challenge.

J Strother Moore, George Porter

ACM Trans. Program. Lang. Syst., 2002

A Grand Challenge Proposal for Formal Methods: A Verified Stack.

J Strother Moore

Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

Single-Threaded Objects in ACL2.

Robert S. Boyer, J Strother Moore

Proceedings of the Practical Aspects of Declarative Languages, 4th International Symposium, 2002

Functional formal methods.

J Strother Moore

Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), 2002

2001

Structured Theory Development for a Mechanized Logic.

Matt Kaufmann, J Strother Moore

J. Autom. Reason., 2001

On the desirability of mechanizing calculational proofs.

Panagiotis Manolios, J Strother Moore

Inf. Process. Lett., 2001

Finite Set Theory in ACL2.

J Strother Moore

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

An Executable Formal Java Virtual Machine Thread Model.

J Strother Moore, George Porter

Proceedings of the 1st Java Virtual Machine Research and Technology Symposium, 2001

Rewriting for Symbolic Execution of State Machine Models.

J Strother Moore

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

1999

A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View.

J Strother Moore

Formal Methods Syst. Des., 1999

Proving Theorems About Java-Like Byte Code.

J Strother Moore

Proceedings of the Correct System Design, 1999

1998

A Mechanically Checked Proof of the AMD5_K86^TM Floating Point Division Program.

J Strother Moore, Thomas W. Lynch, Matt Kaufmann

IEEE Trans. Computers, 1998

Symbolic Simulation: An ACL2 Approach.

J Strother Moore

Proceedings of the Formal Methods in Computer-Aided Design, 1998

An ACL2 Proof of Write Invalidate Cache Coherence.

J Strother Moore

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

A computational logic handbook, Second Edition.

Robert S. Boyer, J Strother Moore

Academic Press international series in formal methods, Academic Press, ISBN: 978-0-12-122955-9, 1998

1997

An Industrial Strength Theorem Prover for a Logic Based on Common Lisp.

Matt Kaufmann, J Strother Moore

IEEE Trans. Software Eng., 1997

1996

ACL2 Theorems About Commercial Microprocessors.

Bishop Brock, Matt Kaufmann, J Strother Moore

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

1994

Introduction to the OBDD Algorithm for the ATP Community.

J Strother Moore

J. Autom. Reason., 1994

A Formal Model of Asynchronous Communication and its Use in Mechanically Verifying a Biphase Mark Protocol.

J Strother Moore

Formal Aspects Comput., 1994

1991

MJRTY: A Fast Majority Vote Algorithm.

Robert S. Boyer, J Strother Moore

Proceedings of the Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991

Functional Instantiation in First-Order Logic.

Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J Strother Moore

Proceedings of the Artificial and Mathematical Theory of Computation, 1991

1990

A Theorem Prover for a Computational Logic.

Robert S. Boyer, J Strother Moore

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

A Mechanically Verified Language Implementation.

J Strother Moore

J. Autom. Reason., 1989

An Approach to Systems Verification.

William R. Bevier, Warren A. Hunt Jr., J Strother Moore, William D. Young

J. Autom. Reason., 1989

1988

The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover.

Robert S. Boyer, J Strother Moore

J. Autom. Reason., 1988

1986

Abstracts in software engineering - reports.

Robert S. Boyer, J Strother Moore, Warren A. Hunt, Richard M. Cohen, Richard C. Holt

ACM SIGSOFT Softw. Eng. Notes, 1986

Overview of a Theorem-Prover for A Computational Logic.

Robert S. Boyer, J Strother Moore

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

A second generation verification environment.

Donald I. Good, Robert S. Boyer, J Strother Moore

ACM SIGSOFT Softw. Eng. Notes, 1985

Program Verification.

Robert S. Boyer, J Strother Moore

J. Autom. Reason., 1985

1984

A Mechanical Proof of the Unsolvability of the Halting Problem.

Robert S. Boyer, J Strother Moore

J. ACM, 1984

1983

Program verification prize.

Robert S. Boyer, J Strother Moore

ACM SIGSOFT Softw. Eng. Notes, 1983

1980

A computational logic.

Robert S. Boyer, J Strother Moore

ACM monograph series, Academic Press, ISBN: 978-0-12-122950-4, 1980

1979

A Mechanical Proof of the Termination of Takeuchi's Function.

J Strother Moore

Inf. Process. Lett., 1979

A computational logic handbook.

Robert S. Boyer, J Strother Moore

Perspectives in computing 23, Academic Press, ISBN: 978-0-12-122952-8, 1979

1977

A Fast String Searching Algorithm.

Robert S. Boyer, J Strother Moore

Commun. ACM, 1977

A Lemma Driven Automatic Theorem Prover for Recursive Function Theory.

Robert S. Boyer, J Strother Moore

Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, 1977

1976

Primitive Recursive Program Transformations.

Robert S. Boyer, J Strother Moore, Robert E. Shostak

Proceedings of the Conference Record of the Third ACM Symposium on Principles of Programming Languages, 1976

1975

Introducing Iteration into the Pure Lisp Theorem Prover.

J Strother Moore

IEEE Trans. Software Eng., 1975

Automatic proof of correctness of a binary addition algorithm.

J Strother Moore

SIGART Newsl., 1975

Proving Theorems about LISP Functions.

Robert S. Boyer, J Strother Moore

J. ACM, 1975

1973

Computational logic : structure sharing and proof of program properties.

J Strother Moore

PhD thesis, 1973