J Strother Moore

90 papers A* 7A 4B 8C 2Journal 35Unranked 27

Year	Rank	Type	Title / Venue / Authors
2025	—	`conf`	Extended Abstract: Partial-encapsulate and Its Support for Floating-point Operations in ACL2. ACL2 Matt Kaufmann, J Strother Moore
2025	J	`jnl`	Rod Burstall: In Memoriam. Formal Aspects Comput. J Strother Moore, Gordon D. Plotkin, David E. Rydeheard, Donald Sannella
2025	J	`jnl`	Rod Bustall: In Memoriam. CoRR J Strother Moore, Gordon D. Plotkin, David E. Rydeheard, Donald Sannella
2024	—	`ch.`	ACL2 Support for Floating-Point Computations. The Practice of Formal Methods (I) Matt Kaufmann, J Strother Moore
2023	—	`conf`	Advances in ACL2 Proof Debugging Tools. ACL2 Matt Kaufmann, J Strother Moore
2022	—	`conf`	VWSIM: A Circuit Simulator. ACL2 Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore
2020	—	`conf`	Iteration in ACL2. ACL2 Matt Kaufmann, J Strother Moore
2020	J	`jnl`	Limited Second-Order Functionality in a First-Order Setting. J. Autom. Reason. Matt Kaufmann, J Strother Moore
2019	J	`jnl`	Milestones from the Pure Lisp theorem prover to ACL2. Formal Aspects Comput. J Strother Moore
2017	J	`jnl`	Automation of Mathematical Induction as part of the History of Logic. FLAP J Strother Moore, Claus-Peter Wirth
2017	—	`ch.`	Computing Verified Machine Address Bounds During Symbolic Exploration of Code. Provably Correct Systems J Strother Moore
2017	—	`conf`	Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions. ARCADE@CADE J Strother Moore, Marijn J. H. Heule
2015	B	`conf`	Machines Reasoning About Machines: 2015. ATVA J Strother Moore
2015	—	`conf`	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States. ACL2 J Strother Moore
2014	—	`conf`	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4. ACL2 Matt Kaufmann, J Strother Moore
2014	B	`conf`	Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete. ITP J Strother Moore
2014	B	`conf`	Rough Diamond: An Extension of Equivalence-Based Rewriting. ITP Matt Kaufmann, J Strother Moore
2013	J	`jnl`	Automation of Mathematical Induction as part of the History of Logic. CoRR J Strother Moore, Claus-Peter Wirth
2013	—	`conf`	Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 ACL2 Matt Kaufmann, J Strother Moore
2012	J	`jnl`	AI meets Formal Software Development (Dagstuhl Seminar 12271). Dagstuhl Reports Alan Bundy, Dieter Hutter, Cliff B. Jones, J Strother Moore
2012	A*	`conf`	Meta-level features in an industrial-strength theorem prover. POPL J Strother Moore
2011	—	`conf`	How Can I Do That with ACL2? Recent Enhancements to ACL2 ACL2 Matt Kaufmann, J Strother Moore
2011	—	`conf`	Reasoning about digital artifacts with ACL2. PLPV J Strother Moore
2011	B	`conf`	The role of human creativity in mechanized verification: FMCAD J Strother Moore
2010	—	`ch.`	ACL2 and Its Applications to Digital System Verification. Design and Verification of Microprocessor Systems for High-Assurance Applications Matt Kaufmann, J Strother Moore
2010	A*	`conf`	Theorem Proving for Verification: The Early Days. LICS J Strother Moore
2009	J	`jnl`	Integrating external deduction tools with ACL2. J. Appl. Log. Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber
2008	J	`jnl`	A Mechanical Analysis of Program Verification Strategies. J. Autom. Reason. Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore
2008	—	`conf`	An ACL2 Tutorial. TPHOLs Matt Kaufmann, J Strother Moore
2008	A	`conf`	An open dialogue concerning the state of education policy in computer science. SIGCSE Robert B. Schnabel, Duncan A. Buell, Joanna Goode, J Strother Moore, Chris Stephenson
2008	J	`jnl`	Efficient execution in an automated reasoning environment. J. Funct. Program. David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding
2008	J	`jnl`	Rewriting with Equivalence Relations in ACL2. J. Autom. Reason. Bishop Brock, Matt Kaufmann, J Strother Moore
2007	—	`conf`	ACL2s: "The ACL2 Sedan". ICSE Companion Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore
2006	—	`conf`	ACL2s: "The ACL2 Sedan". UITP@FLoC Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore
2006	—	`conf`	Double rewriting for equivalential reasoning in ACL2. ACL2 Matt Kaufmann, J Strother Moore
2006	J	`jnl`	Inductive assertions and operational semantics. Int. J. Softw. Tools Technol. Transf. J Strother Moore
2006	B	`conf`	Verification Condition Generation Via Theorem Proving. LPAR John Matthews, J Strother Moore, Sandip Ray, Daron Vroon
2005	—	`conf`	A Mechanized Program Verifier. VSTTE J Strother Moore
2005	J	`jnl`	Executable JVM model for analytical reasoning: A study. Sci. Comput. Program. Hanbing Liu, J Strother Moore
2005	—	`conf`	Meta Reasoning in ACL2. TPHOLs Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
2005	—	`conf`	Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. TPHOLs J Strother Moore, Qiang Zhang
2004	—	`conf`	Java Program Verification via a JVM Deep Embedding in ACL2. TPHOLs Hanbing Liu, J Strother Moore
2004	C	`conf`	On the Adoption of Formal Methods by Industry: The ACL2 Experience. ICFEM J Strother Moore
2004	B	`conf`	Proof Styles in Operational Semantics. FMCAD Sandip Ray, J Strother Moore
2003	—	`conf`	Executable JVM model for analytical reasoning: a study. IVME Hanbing Liu, J Strother Moore
2003	—	`conf`	Inductive Assertions and Operational Semantics. CHARME J Strother Moore
2003	—	`conf`	Linear and Nonlinear Arithmetic in ACL2. CHARME Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore
2003	J	`jnl`	Partial Functions in ACL2. J. Autom. Reason. Panagiotis Manolios, J Strother Moore
2002	—	`conf`	A Grand Challenge Proposal for Formal Methods: A Verified Stack. 10th Anniversary Colloquium of UNU/IIST J Strother Moore
2002	A	`conf`	Functional formal methods. ICFP J Strother Moore
2002	C	`conf`	Single-Threaded Objects in ACL2. PADL Robert S. Boyer, J Strother Moore
2002	J	`jnl`	The apprentice challenge. ACM Trans. Program. Lang. Syst. J Strother Moore, George Porter
2001	—	`conf`	An Executable Formal Java Virtual Machine Thread Model. Java Virtual Machine Research and Technology Symposium J Strother Moore, George Porter
2001	—	`conf`	Finite Set Theory in ACL2. TPHOLs J Strother Moore
2001	J	`jnl`	On the desirability of mechanizing calculational proofs. Inf. Process. Lett. Panagiotis Manolios, J Strother Moore
2001	A*	`conf`	Rewriting for Symbolic Execution of State Machine Models. CAV J Strother Moore
2001	J	`jnl`	Structured Theory Development for a Mechanized Logic. J. Autom. Reason. Matt Kaufmann, J Strother Moore
1999	J	`jnl`	A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View. Formal Methods Syst. Des. J Strother Moore
1999	—	`conf`	Proving Theorems About Java-Like Byte Code. Correct System Design J Strother Moore
1998	J	`jnl`	A Mechanically Checked Proof of the AMD5 IEEE Trans. Computers J Strother Moore, Thomas W. Lynch, Matt Kaufmann
1998	—	`book`	A computational logic handbook, Second Edition. Robert S. Boyer, J Strother Moore
1998	A*	`conf`	An ACL2 Proof of Write Invalidate Cache Coherence. CAV J Strother Moore
1998	B	`conf`	Symbolic Simulation: An ACL2 Approach. FMCAD J Strother Moore
1997	J	`jnl`	An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. Matt Kaufmann, J Strother Moore
1996	B	`conf`	ACL2 Theorems About Commercial Microprocessors. FMCAD Bishop Brock, Matt Kaufmann, J Strother Moore
1994	J	`jnl`	A Formal Model of Asynchronous Communication and its Use in Mechanically Verifying a Biphase Mark Protocol. Formal Aspects Comput. J Strother Moore
1994	J	`jnl`	Introduction to the OBDD Algorithm for the ATP Community. J. Autom. Reason. J Strother Moore
1991	—	`conf`	Functional Instantiation in First-Order Logic. Artificial and Mathematical Theory of Computation Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J Strother Moore
1991	—	`conf`	MJRTY: A Fast Majority Vote Algorithm. Automated Reasoning: Essays in Honor of Woody Bledsoe Robert S. Boyer, J Strother Moore
1990	A	`conf`	A Theorem Prover for a Computational Logic. CADE Robert S. Boyer, J Strother Moore
1989	J	`jnl`	A Mechanically Verified Language Implementation. J. Autom. Reason. J Strother Moore
1989	J	`jnl`	An Approach to Systems Verification. J. Autom. Reason. William R. Bevier, Warren A. Hunt Jr., J Strother Moore, William D. Young
1988	J	`jnl`	The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. J. Autom. Reason. Robert S. Boyer, J Strother Moore
1986	J	`jnl`	Abstracts in software engineering - reports. ACM SIGSOFT Softw. Eng. Notes Robert S. Boyer, J Strother Moore, Warren A. Hunt, Richard M. Cohen, Richard C. Holt
1986	A	`conf`	Overview of a Theorem-Prover for A Computational Logic. CADE Robert S. Boyer, J Strother Moore
1985	J	`jnl`	A second generation verification environment. ACM SIGSOFT Softw. Eng. Notes Donald I. Good, Robert S. Boyer, J Strother Moore
1985	J	`jnl`	Program Verification. J. Autom. Reason. Robert S. Boyer, J Strother Moore
1984	J	`jnl`	A Mechanical Proof of the Unsolvability of the Halting Problem. J. ACM Robert S. Boyer, J Strother Moore
1983	J	`jnl`	Program verification prize. ACM SIGSOFT Softw. Eng. Notes Robert S. Boyer, J Strother Moore
1980	—	`book`	A computational logic. Robert S. Boyer, J Strother Moore
1979	J	`jnl`	A Mechanical Proof of the Termination of Takeuchi's Function. Inf. Process. Lett. J Strother Moore
1979	—	`book`	A computational logic handbook. Robert S. Boyer, J Strother Moore
1977	J	`jnl`	A Fast String Searching Algorithm. Commun. ACM Robert S. Boyer, J Strother Moore
1977	A*	`conf`	A Lemma Driven Automatic Theorem Prover for Recursive Function Theory. IJCAI Robert S. Boyer, J Strother Moore
1976	A*	`conf`	Primitive Recursive Program Transformations. POPL Robert S. Boyer, J Strother Moore, Robert E. Shostak
1975	J	`jnl`	Automatic proof of correctness of a binary addition algorithm. SIGART Newsl. J Strother Moore
1975	J	`jnl`	Introducing Iteration into the Pure Lisp Theorem Prover. IEEE Trans. Software Eng. J Strother Moore
1975	J	`jnl`	Proving Theorems about LISP Functions. J. ACM Robert S. Boyer, J Strother Moore
1973	—	`—`	Computational logic : structure sharing and proof of program properties. J Strother Moore
1973	A*	`conf`	Proving Theorems about LISP Functions. IJCAI Robert S. Boyer, J Strother Moore