Robert S. Boyer | Academic Influence

Robert S. Boyer's AcademicInfluence.com Rankings

Robert S. Boyer

Computer Science

#187

World Rank

#194

Historical Rank

#113

USA Rank

computer-science Degrees

Robert S. Boyer

Mathematics

#1395

World Rank

#2309

Historical Rank

#581

USA Rank

Measure Theory

#2166

World Rank

#2610

Historical Rank

#619

USA Rank

mathematics Degrees

Download Badge

Computer Science
Mathematics

Robert S. Boyer's Degrees

PhD Mathematics University of California, Berkeley
Bachelors Mathematics University of California, Berkeley

Similar Degrees You Can Earn

Best Online Bachelor's in Math 2025

Why Is Robert S. Boyer Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Robert Stephen Boyer is an American retired professor of computer science, mathematics, and philosophy at The University of Texas at Austin. He and J Strother Moore invented the Boyer–Moore string-search algorithm, a particularly efficient string searching algorithm, in 1977. He and Moore also collaborated on the Boyer–Moore automated theorem prover, Nqthm, in 1992. Following this, he worked with Moore and Matt Kaufmann on another theorem prover called ACL2.

(See a Problem?)

Robert S. Boyer'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)
SELECT—a formal system for testing and debugging programs by symbolic execution (1975) (395)
Proving Theorems about LISP Functions (1973) (272)
Efficient implementation of lattice operations (1989) (252)
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)
Pvs: a Prototype Veriication System (1992) (163)
Automated proofs of object code for a widely used microprocessor (1996) (150)
SELECT - a formal system for testing and debugging programs by symbolic execution (1975) (124)
Automated Reasoning: Essays in Honor of Woody Bledsoe (1991) (116)
The Boyer-Moore theorem prover and its interactive enhancement (1995) (109)
Computer Proofs of Limit Theorems (1971) (89)
A Theorem Prover for a Computational Logic (1990) (79)
Functional Instantiation in First-Order Logic (1991) (72)
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)
Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor (1992) (57)
Set theory in first-order logic: Clauses for Gödel's axioms (1986) (53)
A Provably Secure Operating System. (1975) (53)
His Life and Legacy (1996) (51)
Mechanized formal reasoning about programs and computing machines (1997) (48)
A verified code generator for a subset of gypsy (1988) (46)
A Verification Condition Generator for FORTRAN. (1980) (43)
Proof Checking The RSA Public Key Encryption Algorithm (1984) (43)
A Lemma Driven Automatic Theorem Prover for Recursive Function Theory (1977) (42)
Proof-Checking, Theorem Proving, and Program Verification. (1983) (37)
A Mechanical Proof of the Turing Completeness of Pure LISP. (1983) (33)
A computational logic handbook, Second Edition (1998) (32)
Function memoization and unique object representation for ACL2 functions (2006) (30)
Mechanically verifying real-valued algorithms in acl2 (1999) (26)
Woody Bledsoe - His Life and Legacy (1996) (22)
Proceedings of the 1984 ACM Symposium on LISP and functional programming (1982) (22)
PROOF CHECKING THE RSA PUBLIC KEY ENCRYPTION ALGORITHM11The research reported here was supported by National Science Foundation Grant MCS-8202943 and Office of Naval Research Contract N00014-81-K-0634. (1986) (19)
The addition of bounded quantification and partial functions to a computational logic and its theorem prover (1988) (19)
Multi-level secure multicast: the rethinking of secure locks (2002) (18)
A Theorem-Prover for Recursive Functions: A User's Manual. (1979) (18)
The use of a formal simulator to verify a simple real time control program (1990) (16)
Panel Discussion: A Mechanically Proof-Checked Encyclopedia of Mathematics: Should We Build One? Can We? (1994) (13)
A Compressed Format for Collections of Phylogenetic Trees and Improved Consensus Performance (2005) (10)
Overview of a Theorem-Prover for A Computational Logic (1986) (10)
An overview of automated reasoning and related fields (2004) (9)
Investigation, Development, and Evaluation of Performance Proving for Fault-tolerant Computers (1983) (7)
Symbolic simulation in ACL2 (2009) (7)
A Formal Specification of Some User Mode Instructions for The Motorola 68020 (1992) (6)
Locking: A Restriction of Resolution (Dissertation), also ATP-05 (1971) (5)
A computer Proof of the Correctness of a Simple Optimizing Compiler for Expressions. (1977) (4)
Statistics on Criminal Processes (1966) (4)
Primitive recursive program transformation (1976) (4)
A Biographical Sketch of W. W. Bledsoe (1991) (4)
Automated Reasoning (1991) (3)
Mjrty|a Fast Majority Vote Algorithm 1 (1982) (3)
On Why It Is Impossible to Prove that the BDX90 Dispatcher Implements a Time-sharing System (1983) (2)
An Introduction to the System (1988) (2)
Discoveries and experiments in the automation of mathematical reasoning (1997) (1)
Program verification prize (1983) (1)
The Unique Prime Factorization Theorem (1979) (1)
A Formal Semantics for the SRI Hierarchical Program Design Methodology (1983) (1)
Automation of Proof by Mathematical Induction (Dagstuhl Seminar 9530) (2021) (0)
XI – Using Equalities (1979) (0)
A Computational Logic with Quantifiers. (1984) (0)
Rewriting Terms and Simplifying Clauses (1979) (0)
A Precise Description of the Logic (1988) (0)
Delta Hook Tech (Semester Unknown) IPRO 358 (2009) (0)
VIII – Using Definitions (1979) (0)
A Primer for the Logic (1988) (0)
X – Eliminating Destructors (1979) (0)
A Sketch of the Theory and Two Simple Examples (1979) (0)
The Correctness of a Simple Optimizing Expression Compiler (1979) (0)
XIII – Eliminating Irrelevance (1979) (0)
A Precise Definition of the Theory (1979) (0)
Hints on Using the Theorem Prover (1988) (0)
A Sample Session with the Theorem Prover (1988) (0)
Toward Automating the Discovery of Decreasing Measures (2005) (0)
Proof Checking the RSA (Rivest, Shamir and Adleman) Public Key Encryption Algorithm. (1982) (0)
The Correctness of a Tautology-Checker (1979) (0)
14 – Installation Guide (1988) (0)
The Four Classes of Rules Generated from Lemmas (1988) (0)
12 – Reference Guide (1988) (0)
Implementing a Knowledge Date-a-Base (2000) (0)
A second generation verification environment (1985) (0)
Rehosting the Theorem Prover. (1984) (0)
Proving Theorems in the Logic (1988) (0)
Mechanized Proofs in the Logic (1988) (0)
Illustrations of Our Techniques via Elementary Number Theory (1979) (0)
A Fully Automatic Proof of an Ordered Tree Insertion Function. (1983) (0)
Using Axioms and Lemmas as Rewrite Rules (1979) (0)
An Overview of How We Prove Theorems (1979) (0)
Part VII - Formal Models (1988) (0)
How the Theorem Prover Works (1988) (0)
Abstracts in software engineering -- reports (1986) (0)
Caravan and camping sites on the farm. (1980) (0)
Using Type Information to Simplify Formulas (1979) (0)
Note on verification (1989) (0)
The Correctness of a Fast String Searching Algorithm (1979) (0)
Defining of the BDX930 Assembly Language (1983) (0)
Formalization Within the Logic (1988) (0)
Formulating an Induction Scheme for a Conjecture (1979) (0)
Induction and the Analysis of Recursive Definitions (1979) (0)
INTEGRATION PROCESSES COMPARED (2003) (0)

This paper list is powered by the following services:

Other Resources About Robert S. Boyer

en.wikipedia.org

What Schools Are Affiliated With Robert S. Boyer?

Robert S. Boyer is affiliated with the following schools: