dblp.uni-trier.dewww.uni-trier.de

J. Strother Moore Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
53EEMatt Kaufmann, J. Strother Moore, Sandip Ray, Erik Reeber: Integrating external deduction tools with ACL2. J. Applied Logic 7(1): 3-25 (2009)
2008
52EERobert 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
51EEMatt Kaufmann, J. Strother Moore: An ACL2 Tutorial. TPHOLs 2008: 17-21
50EESandip 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)
49EEBishop Brock, Matt Kaufmann, J. Strother Moore: Rewriting with Equivalence Relations in ACL2. J. Autom. Reasoning 40(4): 293-306 (2008)
48EEDavid 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)
2007
47EEPeter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore: ACL2s: "The ACL2 Sedan". ICSE Companion 2007: 59-60
46EEPeter C. Dillinger, Panagiotis Manolios, Daron Vroon, J. Strother Moore: ACL2s: "The ACL2 Sedan". Electr. Notes Theor. Comput. Sci. 174(2): 3-18 (2007)
2006
45EEMatt Kaufmann, J. Strother Moore: Double rewriting for equivalential reasoning in ACL2. ACL2 2006: 103-106
44EEJohn Matthews, J. Strother Moore, Sandip Ray, Daron Vroon: Verification Condition Generation Via Theorem Proving. LPAR 2006: 362-376
43EEJ. Strother Moore: Inductive assertions and operational semantics. STTT 8(4-5): 359-371 (2006)
2005
42EEWarren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith: Meta Reasoning in ACL2. TPHOLs 2005: 163-178
41EEJ. Strother Moore, Qiang Zhang: Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. TPHOLs 2005: 373-384
40EEJ. Strother Moore: A Mechanized Program Verifier. VSTTE 2005: 268-276
39EEHanbing Liu, J. Strother Moore: Executable JVM model for analytical reasoning: A study. Sci. Comput. Program. 57(3): 253-274 (2005)
2004
38EESandip Ray, J. Strother Moore: Proof Styles in Operational Semantics. FMCAD 2004: 67-81
37EEJ. Strother Moore: On the Adoption of Formal Methods by Industry: The ACL2 Experience. ICFEM 2004: 13
36EEHanbing Liu, J. Strother Moore: Java Program Verification via a JVM Deep Embedding in ACL2. TPHOLs 2004: 184-200
2003
35EEJ. Strother Moore: Inductive Assertions and Operational Semantics. CHARME 2003: 289-303
34EEWarren A. Hunt Jr., Robert Bellarmine Krug, J. Strother Moore: Linear and Nonlinear Arithmetic in ACL2. CHARME 2003: 319-333
33EEPanagiotis Manolios, J. Strother Moore: Partial Functions in ACL2. J. Autom. Reasoning 31(2): 107-127 (2003)
2002
32EEJ. Strother Moore: A Grand Challenge Proposal for Formal Methods: A Verified Stack. 10th Anniversary Colloquium of UNU/IIST 2002: 161-172
31EEJ. Strother Moore: Functional formal methods. ICFP 2002: 123
30EERobert S. Boyer, J. Strother Moore: Single-Threaded Objects in ACL2. PADL 2002: 9-27
29EEJ. Strother Moore, George Porter: The apprentice challenge. ACM Trans. Program. Lang. Syst. 24(3): 193-216 (2002)
2001
28EEJ. Strother Moore: Rewriting for Symbolic Execution of State Machine Models. CAV 2001: 411-422
27EEJ. Strother Moore, George Porter: An Executable Formal Java Virtual Machine Thread Model. Java™ Virtual Machine Research and Technology Symposium 2001: 91-104
26EEJ. Strother Moore: Finite Set Theory in ACL2. TPHOLs 2001: 313-328
25EEPanagiotis 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
23EEJ. 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
21EEJ. Strother Moore: An ACL2 Proof of Write Invalidate Cache Coherence. CAV 1998: 29-38
20EEJ. 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
18EEMatt 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
14EERobert 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
10EERobert 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
8EERobert 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)
2EERobert 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

Coauthor Index

1William R. Bevier [13]
2Robert S. Boyer [1] [2] [4] [5] [6] [8] [9] [10] [11] [14] [15] [30]
3Bishop Brock [17] [49]
4Duncan A. Buell [52]
5Peter C. Dillinger [46] [47]
6Joanna Goode [52]
7David A. Greve [48]
8Warren A. Hunt Jr. [13] [34] [42] [50]
9Matt Kaufmann [17] [18] [19] [24] [42] [45] [48] [49] [51] [53]
10Robert Bellarmine Krug [34] [42]
11Hanbing Liu [36] [39]
12Thomas W. Lynch [19]
13Panagiotis Manolios (Pete Manolios) [25] [33] [46] [47] [48]
14John Matthews [44] [50]
15George Porter [27] [29]
16Sandip Ray [38] [44] [48] [50] [53]
17Erik Reeber [53]
18José-Luis Ruiz-Reina [48]
19Robert Schnabel [52]
20Robert E. Shostak [4]
21Eric Whitman Smith [42]
22Chris Stephenson [52]
23Robert W. Sumners (Rob Sumners) [48]
24Daron Vroon [44] [46] [47] [48]
25Matthew Wilding [48]
26William D. Young [13]
27Qiang Zhang [41]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)