Search the dblp DataBase
J. Strother Moore :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Robert S. Boyer , J. Strother Moore A Fast String Searching Algorithm. [Citation Graph (12, 0)][DBLP ] Commun. ACM, 1977, v:20, n:10, pp:762-772 [Journal ] Robert S. Boyer , J. Strother Moore MJRTY: A Fast Majority Vote Algorithm. [Citation Graph (0, 0)][DBLP ] Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991, pp:105-118 [Conf ] J. Strother Moore Proving Theorems About Java-Like Byte Code. [Citation Graph (0, 0)][DBLP ] Correct System Design, 1999, pp:139-162 [Conf ] Robert S. Boyer , J. Strother Moore Overview of a Theorem-Prover for A Computational Logic. [Citation Graph (0, 0)][DBLP ] CADE, 1986, pp:675-678 [Conf ] Robert S. Boyer , J. Strother Moore A Theorem Prover for a Computational Logic. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:1-15 [Conf ] J. Strother Moore Rewriting for Symbolic Execution of State Machine Models. [Citation Graph (0, 0)][DBLP ] CAV, 2001, pp:411-422 [Conf ] J. Strother Moore An ACL2 Proof of Write Invalidate Cache Coherence. [Citation Graph (0, 0)][DBLP ] CAV, 1998, pp:29-38 [Conf ] J. Strother Moore Inductive Assertions and Operational Semantics. [Citation Graph (0, 0)][DBLP ] CHARME, 2003, pp:289-303 [Conf ] Warren A. Hunt Jr. , Robert Bellarmine Krug , J. Strother Moore Linear and Nonlinear Arithmetic in ACL2. [Citation Graph (0, 0)][DBLP ] CHARME, 2003, pp:319-333 [Conf ] Bishop Brock , Matt Kaufmann , J. Strother Moore ACL2 Theorems About Commercial Microprocessors. [Citation Graph (0, 0)][DBLP ] FMCAD, 1996, pp:275-293 [Conf ] J. Strother Moore Symbolic Simulation: An ACL2 Approach. [Citation Graph (0, 0)][DBLP ] FMCAD, 1998, pp:334-350 [Conf ] Sandip Ray , J. Strother Moore Proof Styles in Operational Semantics. [Citation Graph (0, 0)][DBLP ] FMCAD, 2004, pp:67-81 [Conf ] J. Strother Moore On the Adoption of Formal Methods by Industry: The ACL2 Experience. [Citation Graph (0, 0)][DBLP ] ICFEM, 2004, pp:13- [Conf ] J. Strother Moore Functional formal methods. [Citation Graph (0, 0)][DBLP ] ICFP, 2002, pp:123- [Conf ] Robert S. Boyer , J. Strother Moore Proving Theorems about LISP Functions. [Citation Graph (0, 0)][DBLP ] IJCAI, 1973, pp:486-493 [Conf ] Robert S. Boyer , J. Strother Moore A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. [Citation Graph (0, 0)][DBLP ] IJCAI, 1977, pp:511-519 [Conf ] J. Strother Moore , George Porter An Executable Formal Java Virtual Machine Thread Model. [Citation Graph (0, 0)][DBLP ] Java Virtual Machine Research and Technology Symposium, 2001, pp:91-104 [Conf ] John Matthews , J. Strother Moore , Sandip Ray , Daron Vroon Verification Condition Generation Via Theorem Proving. [Citation Graph (0, 0)][DBLP ] LPAR, 2006, pp:362-376 [Conf ] Robert S. Boyer , J. Strother Moore Single-Threaded Objects in ACL2. [Citation Graph (0, 0)][DBLP ] PADL, 2002, pp:9-27 [Conf ] Robert S. Boyer , J. Strother Moore , Robert E. Shostak Primitive Recursive Program Transformations. [Citation Graph (0, 0)][DBLP ] POPL, 1976, pp:171-174 [Conf ] Warren A. Hunt Jr. , Matt Kaufmann , Robert Bellarmine Krug , J. Strother Moore , Eric Whitman Smith Meta Reasoning in ACL2. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2005, pp:163-178 [Conf ] Hanbing Liu , J. Strother Moore Java Program Verification via a JVM Deep Embedding in ACL2. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:184-200 [Conf ] J. Strother Moore Finite Set Theory in ACL2. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:313-328 [Conf ] J. Strother Moore , Qiang Zhang Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2005, pp:373-384 [Conf ] J. Strother Moore A Grand Challenge Proposal for Formal Methods: A Verified Stack. [Citation Graph (0, 0)][DBLP ] 10th Anniversary Colloquium of UNU/IIST, 2002, pp:161-172 [Conf ] Matt Kaufmann , J. Strother Moore Double rewriting for equivalential reasoning in ACL2. [Citation Graph (0, 0)][DBLP ] ACL2, 2006, pp:103-106 [Conf ] Peter C. Dillinger , Panagiotis Manolios , Daron Vroon , J. Strother Moore ACL2s: "The ACL2 Sedan". [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2007, v:174, n:2, pp:3-18 [Journal ] J. Strother Moore A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1999, v:14, n:2, pp:213-228 [Journal ] Panagiotis Manolios , J. Strother Moore On the desirability of mechanizing calculational proofs. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 2001, v:77, n:2-4, pp:173-179 [Journal ] J. Strother Moore A Mechanical Proof of the Termination of Takeuchi's Function. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 1979, v:9, n:4, pp:176-181 [Journal ] Robert S. Boyer , J. Strother Moore Proving Theorems about LISP Functions. [Citation Graph (0, 0)][DBLP ] J. ACM, 1975, v:22, n:1, pp:129-144 [Journal ] Robert S. Boyer , J. Strother Moore A Mechanical Proof of the Unsolvability of the Halting Problem. [Citation Graph (0, 0)][DBLP ] J. ACM, 1984, v:31, n:3, pp:441-458 [Journal ] Robert S. Boyer , J. Strother Moore The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1988, v:4, n:2, pp:117-172 [Journal ] Robert S. Boyer , J. Strother Moore Program Verification. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1985, v:1, n:1, pp:17-23 [Journal ] William R. Bevier , Warren A. Hunt Jr. , J. Strother Moore , William D. Young An Approach to Systems Verification. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1989, v:5, n:4, pp:411-428 [Journal ] Matt Kaufmann , J. Strother Moore Structured Theory Development for a Mechanized Logic. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2001, v:26, n:2, pp:161-203 [Journal ] Panagiotis Manolios , J. Strother Moore Partial Functions in ACL2. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2003, v:31, n:2, pp:107-127 [Journal ] J. Strother Moore A Mechanically Verified Language Implementation. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1989, v:5, n:4, pp:461-492 [Journal ] J. Strother Moore Introduction to the OBDD Algorithm for the ATP Community. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1994, v:12, n:1, pp:33-46 [Journal ] Hanbing Liu , J. Strother Moore Executable JVM model for analytical reasoning: A study. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 2005, v:57, n:3, pp:253-274 [Journal ] J. Strother Moore Inductive assertions and operational semantics. [Citation Graph (0, 0)][DBLP ] STTT, 2006, v:8, n:4-5, pp:359-371 [Journal ] J. Strother Moore , Thomas W. Lynch , Matt Kaufmann A Mechanically Checked Proof of the AMD5K 86TM Floating Point Division Program. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Computers, 1998, v:47, n:9, pp:913-926 [Journal ] J. Strother Moore , George Porter The apprentice challenge. [Citation Graph (0, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 2002, v:24, n:3, pp:193-216 [Journal ] Matt Kaufmann , J. Strother Moore An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Software Eng., 1997, v:23, n:4, pp:203-213 [Journal ] J. Strother Moore Introducing Iteration into the Pure Lisp Theorem Prover. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Software Eng., 1975, v:1, n:3, pp:328-338 [Journal ] Peter C. Dillinger , Panagiotis Manolios , Daron Vroon , J. Strother Moore ACL2s: "The ACL2 Sedan". [Citation Graph (0, 0)][DBLP ] ICSE Companion, 2007, pp:59-60 [Conf ] Theorem Proving for Verification: The Early Days. [Citation Graph (, )][DBLP ] An open dialogue concerning the state of education policy in computer science. [Citation Graph (, )][DBLP ] An ACL2 Tutorial. [Citation Graph (, )][DBLP ] A Mechanized Program Verifier. [Citation Graph (, )][DBLP ] Search in 0.003secs, Finished in 0.154secs