| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | J. Strother Moore |
Meta-level features in an industrial-strength theorem prover.  |
POPL  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J. Strother Moore |
How Can I Do That with ACL2? Recent Enhancements to ACL2 |
ACL2 |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Reasoning about digital artifacts with ACL2. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Theorem Proving for Verification: The Early Days. |
LICS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber |
Integrating external deduction tools with ACL2. |
J. Applied Logic |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Bishop Brock, Matt Kaufmann, J. Strother Moore |
Rewriting with Equivalence Relations in ACL2. |
J. Autom. Reasoning |
2008 |
DBLP DOI BibTeX RDF |
Refinement, Rewriting, Congruence, Equivalence relations |
| 1 | Sandip Ray, Warren A. Hunt Jr., John Matthews, J. Strother Moore |
A Mechanical Analysis of Program Verification Strategies. |
J. Autom. Reasoning |
2008 |
DBLP DOI BibTeX RDF |
Inductive assertions, Partial correctness, Theorem proving, Invariants, Total correctness |
| 1 | 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. |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J. Strother Moore |
An ACL2 Tutorial. |
TPHOLs |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
K-12 curriculum, education policy, teacher certification, STEM |
| 1 | Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore |
ACL2s: "The ACL2 Sedan". |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore |
ACL2s: "The ACL2 Sedan". |
ICSE Companion |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Inductive assertions and operational semantics. |
STTT |
2006 |
DBLP DOI BibTeX RDF |
Theorem proving, JVM, Software verification, Verification condition |
| 1 | John Matthews, J. Strother Moore, Sandip Ray, Daron Vroon |
Verification Condition Generation Via Theorem Proving. |
LPAR |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J. Strother Moore |
Double rewriting for equivalential reasoning in ACL2. |
ACL2 |
2006 |
DBLP DOI BibTeX RDF |
double-rewrite, verification, formal methods, rewriting, congruences, equivalence relations |
| 1 | Hanbing Liu, J. Strother Moore |
Executable JVM model for analytical reasoning: A study. |
Sci. Comput. Program. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
A Mechanized Program Verifier. |
VSTTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith |
Meta Reasoning in ACL2. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore, Qiang Zhang |
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. |
TPHOLs |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
On the Adoption of Formal Methods by Industry: The ACL2 Experience. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Sandip Ray, J. Strother Moore |
Proof Styles in Operational Semantics. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Hanbing Liu, J. Strother Moore |
Java Program Verification via a JVM Deep Embedding in ACL2. |
TPHOLs |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Panagiotis Manolios, J. Strother Moore |
Partial Functions in ACL2. |
J. Autom. Reasoning |
2003 |
DBLP DOI BibTeX RDF |
ACL2, partial functions |
| 1 | J. Strother Moore |
Inductive Assertions and Operational Semantics. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Warren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore |
Linear and Nonlinear Arithmetic in ACL2. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore, George Porter |
The apprentice challenge. |
ACM Trans. Program. Lang. Syst. |
2002 |
DBLP DOI BibTeX RDF |
Java, theorem proving, Java Virtual Machine, mutual exclusion, operational semantics, parallel and distributed computation |
| 1 | Robert S. Boyer, J. Strother Moore |
Single-Threaded Objects in ACL2. |
PADL |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Functional formal methods. |
ICFP |
2002 |
DBLP DOI BibTeX RDF |
functional programming, Java Virtual Machine, microarchitecture, software verification, Common Lisp, hardware verification, mechanical theorem proving |
| 1 | J. Strother Moore |
A Grand Challenge Proposal for Formal Methods: A Verified Stack. |
10th Anniversary Colloquium of UNU/IIST |
2002 |
DBLP DOI BibTeX RDF |
simulation, modeling, model checking, theorem proving, software verification, hardware verification |
| 1 | Panagiotis Manolios, J. Strother Moore |
On the desirability of mechanizing calculational proofs. |
Inf. Process. Lett. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J. Strother Moore |
Structured Theory Development for a Mechanized Logic. |
J. Autom. Reasoning |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore, George Porter |
An Executable Formal Java Virtual Machine Thread Model. |
Java Virtual Machine Research and Technology Symposium |
2001 |
DBLP BibTeX RDF |
|
| 1 | J. Strother Moore |
Finite Set Theory in ACL2. |
TPHOLs |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Rewriting for Symbolic Execution of State Machine Models. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
microprocessor simulation, pipelined machine, verification, theorem proving, Hardware modeling |
| 1 | J. Strother Moore |
A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View. |
Formal Methods in System Design |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Proving Theorems About Java-Like Byte Code. |
Correct System Design |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore, Thomas W. Lynch, Matt Kaufmann |
A Mechanically Checked Proof of the AMD5K86TM Floating Point Division Program. |
IEEE Trans. Computers |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
A computational logic handbook (2. ed.). |
|
1998 |
RDF |
|
| 1 | J. Strother Moore |
Symbolic Simulation: An ACL2 Approach. |
FMCAD |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
An ACL2 Proof of Write Invalidate Cache Coherence. |
CAV |
1998 |
DBLP DOI BibTeX RDF |
|
| 1 | Matt Kaufmann, J. Strother Moore |
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. |
IEEE Trans. Software Eng. |
1997 |
DBLP DOI BibTeX RDF |
total functions, microcode verification, floating point division, Formal verification, digital signal processing, type checking, computational logic, automatic theorem proving, partial functions |
| 1 | Bishop Brock, Matt Kaufmann, J. Strother Moore |
ACL2 Theorems About Commercial Microprocessors. |
FMCAD |
1996 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
Introduction to the OBDD Algorithm for the ATP Community. |
J. Autom. Reasoning |
1994 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
MJRTY: A Fast Majority Vote Algorithm. |
Automated Reasoning: Essays in Honor of Woody Bledsoe |
1991 |
DBLP BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
A Theorem Prover for a Computational Logic. |
CADE |
1990 |
DBLP DOI BibTeX RDF |
|
| 1 | J. Strother Moore |
A Mechanically Verified Language Implementation. |
J. Autom. Reasoning |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | William R. Bevier, Warren A. Hunt Jr., J. Strother Moore, William D. Young |
An Approach to Systems Verification. |
J. Autom. Reasoning |
1989 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
1988 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
Overview of a Theorem-Prover for A Computational Logic. |
CADE |
1986 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
Program Verification. |
J. Autom. Reasoning |
1985 |
DBLP BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
A Mechanical Proof of the Unsolvability of the Halting Problem. |
J. ACM |
1984 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
A computational logic. |
|
1980 |
RDF |
|
| 1 | J. Strother Moore |
A Mechanical Proof of the Termination of Takeuchi's Function. |
Inf. Process. Lett. |
1979 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
A Fast String Searching Algorithm. |
Commun. ACM |
1977 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. |
IJCAI |
1977 |
DBLP BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore, Robert E. Shostak |
Primitive Recursive Program Transformations. |
POPL |
1976 |
DBLP DOI BibTeX RDF |
Theorem proving, Program verification, LISP, LISP, Flowcharts, Structural induction |
| 1 | J. Strother Moore |
Introducing Iteration into the Pure Lisp Theorem Prover. |
IEEE Trans. Software Eng. |
1975 |
DBLP BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
Proving Theorems about LISP Functions. |
J. ACM |
1975 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert S. Boyer, J. Strother Moore |
Proving Theorems about LISP Functions. |
IJCAI |
1973 |
DBLP BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")