| A fast string searching algorithm RS Boyer, JS Moore Communications of the ACM 20 (10), 762-772, 1977 | 4027 | 1977 |
| A computational logic RS Boyer, JS Moore Academic press, 2014 | 1943 | 2014 |
| A computational logic handbook: Formerly notes and reports in computer science and applied mathematics RS Boyer, JS Moore Elsevier, 2014 | 1206 | 2014 |
| Computer-aided reasoning: ACL2 case studies M Kaufmann, P Manolios, JS Moore Springer Science & Business Media, 2013 | 1106 | 2013 |
| MJRTY—a fast majority vote algorithm RS Boyer, JS Moore Automated reasoning: essays in honor of Woody Bledsoe, 105-117, 1991 | 393 | 1991 |
| Proving theorems about LISP functions RS Boyer, JS Moore Journal of the ACM (JACM) 22 (1), 129-144, 1975 | 360 | 1975 |
| An industrial strength theorem prover for a logic based on Common Lisp M Kaufmann, JS Moore IEEE Transactions on Software Engineering 23 (4), 203-213, 1997 | 322 | 1997 |
| The sharing structure in theorem-proving programs. R Boyer Machine intelligence 7, 101-116, 1972 | 284 | 1972 |
| Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic RS Boyer, JS Moore Machine intelligence 11, 83-124, 1988 | 255 | 1988 |
| An approach to systems verification WR Bevier, WA Hunt, JS Moore, WD Young Journal of Automated Reasoning 5, 411-428, 1989 | 230 | 1989 |
| A mechanically checked proof of the AMD5K86TM floating-point division program JS Moore, TW Lynch, M Kaufmann IEEE Transactions on Computers 47 (09), 913-926, 1998 | 214 | 1998 |
| ACL2: An industrial strength version of Nqthm M Kaufmann, JS Moore Proceedings of 11th Annual Conference on Computer Assurance. COMPASS'96, 23-34, 1996 | 209 | 1996 |
| Metafunctions: proving them correct and using them efficiently as new proof procedures RS Boyer, JS Moore SRI International, Computer Science Laboratory, 1979 | 207 | 1979 |
| ACL2 theorems about commercial microprocessors B Brock, M Kaufmann, JS Moore International Conference on Formal Methods in Computer-Aided Design, 275-293, 1996 | 202 | 1996 |
| A mechanically verified language implementation JS Moore Journal of Automated Reasoning 5 (4), 461-492, 1989 | 189 | 1989 |
| The Boyer-Moore theorem prover and its interactive enhancement RS Boyer, M Kaufmann, JS Moore Computers & Mathematics with Applications 29 (2), 27-62, 1995 | 161 | 1995 |
| Piton: a mechanically verified assembly-level language JS Moore Springer, 2007 | 125 | 2007 |
| System verification JS Moore Journal of Automated Reasoning 5 (4), 409-410, 1989 | 120 | 1989 |
| Mechanical stretch activates nuclear factor‐kappaB, activator protein‐1, and mitogen‐activated protein kinases in lung parenchyma: implications in asthma A Kumar, S Lnu, R Malya, D Barron, J Moore, DB Corry, AM Boriek The FASEB journal 17 (13), 1800-1811, 2003 | 119 | 2003 |
| Structured theory development for a mechanized logic M Kaufmann, JS Moore Journal of Automated Reasoning 26, 161-203, 2001 | 112 | 2001 |
