| 2009 |
|---|
| 53 | EE | Matt Kaufmann,
J. Strother Moore,
Sandip Ray,
Erik Reeber:
Integrating external deduction tools with ACL2.
J. Applied Logic 7(1): 3-25 (2009) |
| 2008 |
|---|
| 52 | EE | 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 |
| 51 | EE | Matt Kaufmann,
J. Strother Moore:
An ACL2 Tutorial.
TPHOLs 2008: 17-21 |
| 50 | EE | 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) |
| 49 | EE | Bishop Brock,
Matt Kaufmann,
J. Strother Moore:
Rewriting with Equivalence Relations in ACL2.
J. Autom. Reasoning 40(4): 293-306 (2008) |
| 48 | EE | David A. Greve,
Matt Kaufmann,
Panagiotis Manolios,
J. Strother Moore,
Sandip Ray,
José-Luis Ruiz-Reina,
R. O. B. Sumners,
Daron Vroon,
Matthew Wilding:
Efficient execution in an automated reasoning environment.
J. Funct. Program. 18(1): 15-46 (2008) |
| 2007 |
|---|
| 47 | EE | Peter C. Dillinger,
Panagiotis Manolios,
Daron Vroon,
J. Strother Moore:
ACL2s: "The ACL2 Sedan".
ICSE Companion 2007: 59-60 |
| 46 | EE | Peter C. Dillinger,
Panagiotis Manolios,
Daron Vroon,
J. Strother Moore:
ACL2s: "The ACL2 Sedan".
Electr. Notes Theor. Comput. Sci. 174(2): 3-18 (2007) |
| 2006 |
|---|
| 45 | EE | Matt Kaufmann,
J. Strother Moore:
Double rewriting for equivalential reasoning in ACL2.
ACL2 2006: 103-106 |
| 44 | EE | John Matthews,
J. Strother Moore,
Sandip Ray,
Daron Vroon:
Verification Condition Generation Via Theorem Proving.
LPAR 2006: 362-376 |
| 43 | EE | J. Strother Moore:
Inductive assertions and operational semantics.
STTT 8(4-5): 359-371 (2006) |
| 2005 |
|---|
| 42 | EE | Warren A. Hunt Jr.,
Matt Kaufmann,
Robert Bellarmine Krug,
J. Strother Moore,
Eric Whitman Smith:
Meta Reasoning in ACL2.
TPHOLs 2005: 163-178 |
| 41 | EE | J. Strother Moore,
Qiang Zhang:
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2.
TPHOLs 2005: 373-384 |
| 40 | EE | J. Strother Moore:
A Mechanized Program Verifier.
VSTTE 2005: 268-276 |
| 39 | EE | Hanbing Liu,
J. Strother Moore:
Executable JVM model for analytical reasoning: A study.
Sci. Comput. Program. 57(3): 253-274 (2005) |
| 2004 |
|---|
| 38 | EE | Sandip Ray,
J. Strother Moore:
Proof Styles in Operational Semantics.
FMCAD 2004: 67-81 |
| 37 | EE | J. Strother Moore:
On the Adoption of Formal Methods by Industry: The ACL2 Experience.
ICFEM 2004: 13 |
| 36 | EE | Hanbing Liu,
J. Strother Moore:
Java Program Verification via a JVM Deep Embedding in ACL2.
TPHOLs 2004: 184-200 |
| 2003 |
|---|
| 35 | EE | J. Strother Moore:
Inductive Assertions and Operational Semantics.
CHARME 2003: 289-303 |
| 34 | EE | Warren A. Hunt Jr.,
Robert Bellarmine Krug,
J. Strother Moore:
Linear and Nonlinear Arithmetic in ACL2.
CHARME 2003: 319-333 |
| 33 | EE | Panagiotis Manolios,
J. Strother Moore:
Partial Functions in ACL2.
J. Autom. Reasoning 31(2): 107-127 (2003) |
| 2002 |
|---|
| 32 | EE | J. Strother Moore:
A Grand Challenge Proposal for Formal Methods: A Verified Stack.
10th Anniversary Colloquium of UNU/IIST 2002: 161-172 |
| 31 | EE | J. Strother Moore:
Functional formal methods.
ICFP 2002: 123 |
| 30 | EE | Robert S. Boyer,
J. Strother Moore:
Single-Threaded Objects in ACL2.
PADL 2002: 9-27 |
| 29 | EE | J. Strother Moore,
George Porter:
The apprentice challenge.
ACM Trans. Program. Lang. Syst. 24(3): 193-216 (2002) |
| 2001 |
|---|
| 28 | EE | J. Strother Moore:
Rewriting for Symbolic Execution of State Machine Models.
CAV 2001: 411-422 |
| 27 | EE | J. Strother Moore,
George Porter:
An Executable Formal Java Virtual Machine Thread Model.
Java™ Virtual Machine Research and Technology Symposium 2001: 91-104 |
| 26 | EE | J. Strother Moore:
Finite Set Theory in ACL2.
TPHOLs 2001: 313-328 |
| 25 | EE | Panagiotis Manolios,
J. Strother Moore:
On the desirability of mechanizing calculational proofs.
Inf. Process. Lett. 77(2-4): 173-179 (2001) |
| 24 | | Matt Kaufmann,
J. Strother Moore:
Structured Theory Development for a Mechanized Logic.
J. Autom. Reasoning 26(2): 161-203 (2001) |
| 1999 |
|---|
| 23 | EE | J. Strother Moore:
Proving Theorems About Java-Like Byte Code.
Correct System Design 1999: 139-162 |
| 22 | | 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) |
| 1998 |
|---|
| 21 | | J. Strother Moore:
An ACL2 Proof of Write Invalidate Cache Coherence.
CAV 1998: 29-38 |
| 20 | EE | J. Strother Moore:
Symbolic Simulation: An ACL2 Approach.
FMCAD 1998: 334-350 |
| 19 | | J. Strother Moore,
Thomas W. Lynch,
Matt Kaufmann:
A Mechanically Checked Proof of the AMD5K86TM Floating Point Division Program.
IEEE Trans. Computers 47(9): 913-926 (1998) |
| 1997 |
|---|
| 18 | EE | 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) |
| 1996 |
|---|
| 17 | | Bishop Brock,
Matt Kaufmann,
J. Strother Moore:
ACL2 Theorems About Commercial Microprocessors.
FMCAD 1996: 275-293 |
| 1994 |
|---|
| 16 | | J. Strother Moore:
Introduction to the OBDD Algorithm for the ATP Community.
J. Autom. Reasoning 12(1): 33-46 (1994) |
| 1991 |
|---|
| 15 | | Robert S. Boyer,
J. Strother Moore:
MJRTY: A Fast Majority Vote Algorithm.
Automated Reasoning: Essays in Honor of Woody Bledsoe 1991: 105-118 |
| 1990 |
|---|
| 14 | | Robert S. Boyer,
J. Strother Moore:
A Theorem Prover for a Computational Logic.
CADE 1990: 1-15 |
| 1989 |
|---|
| 13 | | 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) |
| 12 | | J. Strother Moore:
A Mechanically Verified Language Implementation.
J. Autom. Reasoning 5(4): 461-492 (1989) |
| 1988 |
|---|
| 11 | | 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) |
| 1986 |
|---|
| 10 | | Robert S. Boyer,
J. Strother Moore:
Overview of a Theorem-Prover for A Computational Logic.
CADE 1986: 675-678 |
| 1985 |
|---|
| 9 | | Robert S. Boyer,
J. Strother Moore:
Program Verification.
J. Autom. Reasoning 1(1): 17-23 (1985) |
| 1984 |
|---|
| 8 | EE | Robert S. Boyer,
J. Strother Moore:
A Mechanical Proof of the Unsolvability of the Halting Problem.
J. ACM 31(3): 441-458 (1984) |
| 1979 |
|---|
| 7 | | J. Strother Moore:
A Mechanical Proof of the Termination of Takeuchi's Function.
Inf. Process. Lett. 9(4): 176-181 (1979) |
| 1977 |
|---|
| 6 | | Robert S. Boyer,
J. Strother Moore:
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory.
IJCAI 1977: 511-519 |
| 5 | | Robert S. Boyer,
J. Strother Moore:
A Fast String Searching Algorithm.
Commun. ACM 20(10): 762-772 (1977) |
| 1976 |
|---|
| 4 | | Robert S. Boyer,
J. Strother Moore,
Robert E. Shostak:
Primitive Recursive Program Transformations.
POPL 1976: 171-174 |
| 1975 |
|---|
| 3 | | J. Strother Moore:
Introducing Iteration into the Pure Lisp Theorem Prover.
IEEE Trans. Software Eng. 1(3): 328-338 (1975) |
| 2 | EE | Robert S. Boyer,
J. Strother Moore:
Proving Theorems about LISP Functions.
J. ACM 22(1): 129-144 (1975) |
| 1973 |
|---|
| 1 | | Robert S. Boyer,
J. Strother Moore:
Proving Theorems about LISP Functions.
IJCAI 1973: 486-493 |
