J Strother Moore | Academic Influence

J Strother Moore's AcademicInfluence.com Rankings

J Strother Moore

Computer Science

#192

World Rank

#199

Historical Rank

#116

USA Rank

Database

#1811

World Rank

#1899

Historical Rank

#453

USA Rank

computer-science Degrees

Download Badge

Computer Science

J Strother Moore's Degrees

Masters Mathematics Stanford University
Bachelors Mathematics California Institute of Technology

Similar Degrees You Can Earn

Best Online Bachelor's in Math 2025

Why Is J Strother Moore Influential?

(Suggest an Edit or Addition)

According to Wikipedia, J Strother Moore is a computer scientist. He is a co-developer of the Boyer–Moore string-search algorithm, Boyer–Moore majority vote algorithm, and the Boyer–Moore automated theorem prover, Nqthm. He made pioneering contributions to structure sharing including the piece table data structure and early logic programming. An example of the workings of the Boyer–Moore string search algorithm is given in Moore's website. Moore received his Bachelor of Science in mathematics at Massachusetts Institute of Technology in 1970 and his Doctor of Philosophy in computational logic at the University of Edinburgh in Scotland in 1973.

(See a Problem?)

J Strother Moore's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

A fast string searching algorithm (1977) (2525)
Computational Logic (1990) (1109)
A computational logic handbook (1979) (828)
Computer-Aided Reasoning: An Approach (2011) (401)
Proving Theorems about LISP Functions (1973) (272)
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp (1997) (272)
Computer-aided reasoning : ACL2 case studies (2000) (265)
The Correctness Problem in Computer Science (1982) (250)
MJRTY: A Fast Majority Vote Algorithm (1991) (231)
Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic (1988) (196)
Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures. (1979) (165)
ACL2 Theorems About Commercial Microprocessors (1996) (160)
The Boyer-Moore theorem prover and its interactive enhancement (1995) (109)
An approach to systems verification (1989) (104)
A Mechanically Checked Proof of the AMD5K86TM Floating Point Division Program (1998) (102)
A mechanically verified language implementation (1989) (97)
Ttle sharing of structure in theorem proving programs (1972) (92)
Structured Theory Development for a Mechanized Logic (2001) (83)
A Mechanically Checked Proof of the (1998) (81)
A Theorem Prover for a Computational Logic (1990) (79)
Piton: A Mechanically Verified Assembly-Level Language (1996) (77)
Functional Instantiation in First-Order Logic (1991) (72)
Symbolic Simulation: An ACL2 Approach (1998) (71)
Program Verification (1985) (70)
A verified operating system kernel (1987) (64)
A Mechanical Proof of the Unsolvability of the Halting Problem (1984) (64)
Single-Threaded Objects in ACL2 (2002) (62)
A Grand Challenge Proposal for Formal Methods: A Verified Stack (2002) (60)
Partial Functions in ACL2 (2003) (58)
Executable JVM model for analytical reasoning: a study (2003) (53)
A Mechanically Checked Proof of the Correctness of the Kernel of the Amd5 K 86 Tm Floating-point Division Algorithm (1996) (52)
Java Program Verification via a JVM Deep Embedding in ACL2 (2004) (50)
Mechanized formal reasoning about programs and computing machines (1997) (48)
A verified code generator for a subset of gypsy (1988) (46)
ACL2s: "The ACL2 Sedan" (2007) (46)
Verification Condition Generation Via Theorem Proving (2006) (45)
Computational logic : structure sharing and proof of program properties (1973) (45)
Proof Checking The RSA Public Key Encryption Algorithm (1984) (43)
Computer-Aided Reasoning (2000) (43)
A Verification Condition Generator for FORTRAN. (1980) (43)
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory (1977) (42)
Efficient execution in an automated reasoning environment (2008) (39)
Industrial hardware and software verification with ACL2 (2017) (38)
Inductive assertions and operational semantics (2003) (37)
Proof-Checking, Theorem Proving, and Program Verification. (1983) (37)
Meta Reasoning in ACL2 (2005) (37)
A Precise Description of the ACL2 Logic (1998) (36)
The apprentice challenge (2002) (35)
Linear and Nonlinear Arithmetic in ACL2 (2003) (33)
A Mechanical Proof of the Turing Completeness of Pure LISP. (1983) (33)
A computational logic handbook, Second Edition (1998) (32)
Proving Theorems About Java-Like Byte Code (1999) (30)
A Mechanical Proof of the Termination of Takeuchi's Function (1979) (29)
Integrating external deduction tools with ACL2 (2006) (28)
An ACL2 Tutorial (2008) (27)
Introducing iteration into the Pure Lisp theorem prover (1975) (25)
Proof Styles in Operational Semantics (2004) (24)
A Mechanically Checked Proof of a Multiprocessor Result via a Uniprocessor View (1999) (24)
The INTERLISP Virtual Machine Specification (1976) (23)
System verification (1989) (23)
Introduction to the OBDD algorithm for the ATP community (1994) (23)
A self-verifying theorem prover (2009) (22)
A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol (2005) (22)
The addition of bounded quantification and partial functions to a computational logic and its theorem prover (1988) (19)
Milestones from the Pure Lisp theorem prover to ACL2 (2019) (18)
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2 (2005) (18)
A Theorem-Prover for Recursive Functions: A User's Manual. (1979) (18)
A Computational Logic for Applicative Common LISP (2007) (17)
The use of a formal simulator to verify a simple real time control program (1990) (16)
Rewriting with Equivalence Relations in ACL2 (2008) (14)
A Mechanical Analysis of Program Verification Strategies (2008) (12)
An Executable Formal Java Virtual Machine Thread Model (2001) (12)
Formal specification and verification of a jvm and its bytecode verifier (2006) (12)
An ACL2 Proof of Write Invalidate Cache Coherence (1998) (11)
Rewriting for Symbolic Execution of State Machine Models (2001) (10)
An exercise in graph theory (2000) (10)
Overview of a Theorem-Prover for A Computational Logic (1986) (10)
A Mechanized Program Verifier (2005) (10)
An overview of automated reasoning and related fields (2004) (9)
A Mechanically Checked Proof of a Comparator Sort Algorithm (2005) (8)
AI meets Formal Software Development (Dagstuhl Seminar 12271) (2012) (7)
Investigation, Development, and Evaluation of Performance Proving for Fault-tolerant Computers (1983) (7)
Finite Set Theory in ACL2 (2001) (7)
Rough Diamond: An Extension of Equivalence-Based Rewriting (2014) (6)
Should We Begin a Standardization Process for Interface Logics (1992) (6)
Integrating CCG Analysis into ACL 2 ⋆ (2006) (6)
Functional formal methods (2002) (6)
Automatic proof of correctness of a binary addition algorithm (1975) (6)
Stateman: Using Metafunctions to Manage Large Terms Representing Machine States (2015) (6)
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 (2013) (5)
How Can I Do That with ACL2? Recent Enhancements to ACL2 (2011) (5)
On the desirability of mechanizing calculational proofs (2001) (5)
Proof Search Debugging Tools in ACL 2 (2008) (5)
Theorem Proving for Verification: The Early Days (2010) (4)
A computer Proof of the Correctness of a Simple Optimizing Compiler for Expressions. (1977) (4)
Limited Second-Order Functionality in a First-Order Setting (2018) (4)
Primitive recursive program transformation (1976) (4)
Basic principles of mechanical theorem proving in elementary geometries (Editors preface) (1986) (3)
Double rewriting for equivalential reasoning in ACL2 (2006) (3)
Mjrty|a Fast Majority Vote Algorithm 1 (1982) (3)
Meta Reasoning in ACL 2 (3)
A Symbolic Simulation Approach to Assertional Program Verification (2005) (3)
Automatically computing functional instantiations (2009) (3)
Well-Formedness Guarantees for ACL2 Metafunctions and Clause Processors (2015) (3)
Proof Pearl : Dijkstra ' s Shortest Path AlgorithmVeri ed with ACL 2 (2005) (2)
On Why It Is Impossible to Prove that the BDX90 Dispatcher Implements a Time-sharing System (1983) (2)
Mechanized Operational Semantics : The M 1 Story (2008) (2)
An Introduction to the System (1988) (2)
Industrially Sponsored University Research in Information Technology : Some Recommendations Regarding Intellectual Property Agreements (2)
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (2014) (2)
Maintaining the ACL2 theorem proving system (2006) (2)
ACL2 and Its Applications to Digital System Verification (2010) (2)
Industrial Proofs with ACL 2 (2005) (2)
The Role of Automated Reasoning in Integrated System Verification Environments (2006) (2)
Iteration in ACL2 (2020) (2)
An open dialogue concerning the state of education policy in computer science (2008) (2)
Think It Through (2015) (2)
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (2014) (2)
Computing Verified Machine Address Bounds During Symbolic Exploration of Code (2017) (2)
Using theorem proving and algorithmic decision procedures for large-scale system verification (2005) (2)
Industrial Use of ACL2: Applications, Achievements, Challenges, and Directions (2017) (1)
Specifications in Software Development (1992) (1)
The role of human creativity in mechanized verification (2011) (1)
Meta-level features in an industrial-strength theorem prover (2012) (1)
An Extension of Equivalence-based Rewriting (2014) (1)
Generalization, lemma generation, and induction in acl2 (2008) (1)
Program verification: an approach to reliable hardware and software (1980) (1)
Towards a mechanically checked theory of computation: the ACL2 project (2000) (1)
Machines Reasoning About Machines: 2015 (2015) (1)
Towards a mechanically checked theory of computation (2001) (1)
ACL2 Workshop 2000 Proceedings, Part A (2000) (1)
Learning the Rules (2011) (1)
The Unique Prime Factorization Theorem (1979) (1)
A Formal Semantics for the SRI Hierarchical Program Design Methodology (1983) (1)
ACL2 essentials (2000) (1)
Program verification prize (1983) (1)
Mechanized Proofs in the Logic (1988) (0)
X – Eliminating Destructors (1979) (0)
ACL2 Workshop 2000 Proceedings, Part B, Goerigk-Kaufman (2000) (0)
How to Use the Theorem Prover (2000) (0)
Even Older Games (2015) (0)
A second generation verification environment (1985) (0)
Formulating an Induction Scheme for a Conjecture (1979) (0)
Restless for More (2015) (0)
Proving Theorems in the Logic (1988) (0)
A Suite of Tools for Analyzing ACL2 Books (2010) (0)
XI – Using Equalities (1979) (0)
Hints on Using the Theorem Prover (1988) (0)
On the Adoption of Formal Methods by Industry: The ACL2 Experience (2004) (0)
Reasoning about digital artifacts with ACL2 (2011) (0)
Rehosting the Theorem Prover. (1984) (0)
Illustrations of Our Techniques via Elementary Number Theory (1979) (0)
Theorem Prover Examples (2000) (0)
ACL2 Workshop 2000 Proceedings, Part A, Lusk et al-Ruiz-Reina et al (2000) (0)
A Computational Logic with Quantifiers. (1984) (0)
Three Lectures on Theorem-proving and Program Verification (1983) (0)
A Precise Description of the Logic (1988) (0)
On the desirability of me hanizing al ulational (0)
An Overview of How We Prove Theorems (1979) (0)
Rewriting Terms and Simplifying Clauses (1979) (0)
How the Theorem Prover Works (1988) (0)
Verification of transformation rules of the higher-order transformation language tl (2005) (0)
Theorem Prover Exercises (2000) (0)
A Primer for the Logic (1988) (0)
Formalization Within the Logic (1988) (0)
Using Type Information to Simplify Formulas (1979) (0)
General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software (2000) (0)
The Proof of the Pudding (2015) (0)
The Correctness of a Simple Optimizing Expression Compiler (1979) (0)
A Sketch of the Theory and Two Simple Examples (1979) (0)
XIII – Eliminating Irrelevance (1979) (0)
Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (2022) (0)
Old Games, New Rules (2015) (0)
Think It Over, and Over, and Over (2015) (0)
Induction and the Analysis of Recursive Definitions (1979) (0)
The Correctness of a Tautology-Checker (1979) (0)
Proof Checking the RSA (Rivest, Shamir and Adleman) Public Key Encryption Algorithm. (1982) (0)
A Sample Session with the Theorem Prover (1988) (0)
Summaries of the Case Studies (2000) (0)
The Little Assistant (2015) (0)
14 – Installation Guide (1988) (0)
12 – Reference Guide (1988) (0)
The Four Classes of Rules Generated from Lemmas (1988) (0)
Editor's preface to ‘basic principles of mechanical theorem proving in elementary geometries’ by Wu Wen-tsun (2006) (0)
Milestones from The Pure Lisp Theorem Prover to ACL 2 Draft 4 – 5 March , 2019 (2019) (0)
Problems in Automated Theorem Proving for Hardware and Software Verification (0)
Changing the Rules (2015) (0)
Using Axioms and Lemmas as Rewrite Rules (1979) (0)
The Stars Are Aligned (2015) (0)
Bounds during Symbolic Exploration of Code (2016) (0)
Limited Second-Order Functionality in a First-Order Setting (2018) (0)
Abstracts in software engineering -- reports (1986) (0)
Proving Properties of Java Threads (2011) (0)
Exemplary Achievements Industrial Use of ACL 2 : Applications , Achievements , Challenges , and Directions (2017) (0)
ACL2 Induction Heuristics (2020) (0)
SPECIAL SECTION ON RECENT ADVANCES IN HARDWARE VERIFICATION (0)
Building Software Systems Economically with Mechanized Logic: Initial Design Proposal (1987) (0)
Oh My, Stars! (2015) (0)
Functional formal methods: Invited talk (2002) (0)
Part of This Total Breakfast (2015) (0)
A Fully Automatic Proof of an Ordered Tree Insertion Function. (1983) (0)
VIII – Using Definitions (1979) (0)
The Correctness of a Fast String Searching Algorithm (1979) (0)
The Mechanical Theorem Prover (2000) (0)
Defining of the BDX930 Assembly Language (1983) (0)
A Precise Definition of the Theory (1979) (0)
Recollections of Hope Park Square, 1970–1973 (2021) (0)

This paper list is powered by the following services:

Other Resources About J Strother Moore

en.wikipedia.org

What Schools Are Affiliated With J Strother Moore?

J Strother Moore is affiliated with the following schools:

Image Attributions

Image Source for J Strother Moore