# Milestones from the Pure Lisp theorem prover to ACL2

- 35 Downloads
- 1 Citations

## Abstract

We discuss the evolutionary path from the Edinburgh Pure Lisp Theorem Prover of the early 1970s to its modern counterpart, *A**C*omputational *L*ogic for *A*pplicative *C*ommon *L*isp, aka ACL2, which is in regular industrial use. Among the milestones in this evolution are the adoption of a first-order subset of a programming language as a logic; the analysis of recursive definitions to guess appropriate mathematical induction schemes; the use of simplification in inductive proofs; the incorporation of rewrite rules derived from user-suggested lemmas; the generalization of that idea to allow the user to affect other proof techniques soundly; the recognition that evaluation efficiency is paramount so that formal models can serve as prototypes and the logic can be used to reprogram the system; use of the system to prove extensions correct; the incorporation of decision procedures; the provision of hierarchically structured libraries of previously certified results to configure the prover; the provision of system programming features to allow verification tools to be built and verified within the system; the release of many verified collections of lemmas supporting floating point, programming languages, and hardware platforms; a verified “bit-bashing” tool exploiting verified BDD and checked external SAT procedures; and the provision
of certain higher-order features within the first-order setting. As will become apparent, some of these milestones were suggested or even prototyped by users. Some additional non-technical aspects of the project are also critical. Among these are a devotion to soundness, good documentation, freely available source code, production of a system usable by industry, responsiveness to user needs, and a dedicated, passionate, and brilliant user community.

## Keywords

Theorem proving Hardware Software Verification Functional programming Lisp Induction Rewriting Reflection Decision procedures## Preview

Unable to display preview. Download preview PDF.

## Notes

### Acknowledgments

I thank Bob Boyer, Matt Kaufmann, and Grant Passmore for their careful readings of early versions of this manuscript; all remaining mistakes are mine. I thank the formal reviewers of this article who, by raising many questions, have made this a more complete history. I also thank Cliff Jones for inviting me to write this article. A list of important sponsors and contributors to the ACL2 project may be found online \(\lceil\)acknowledgments\(\rceil\).

Bob Boyer and Matt Kaufmann are as much a part of this story as I am. I am incredibly lucky to have found two such research partners and I am deeply grateful to both of them. The users of Nqthm and ACL2, especially the students who joined us in the UT Tower in the 1980s deserve a great deal of thanks too. They pushed Nqthm to its limits. Many of those students then moved to CLI with us and switched to ACL2 and have proceeded to push it, repeatedly, to its limits. ACL2 would not exist had it not been for these people. I am humbled and deeply grateful for their passion, patience, and persistence.

## References

- BB74.Bledsoe, W.W., Bruell, P.: A man-machine theorem-proving system. Artif Intell
**5**, 51–72 (1974)MathSciNetCrossRefGoogle Scholar - BDM73.Boyer RS, Davies DJM, Moore JS (1973) The 77-editor. Technical Report 62, Department of Computational Logic, University of EdinburghGoogle Scholar
- BGKM91.Boyer RS, Goldschlag DM, Kaufmann M, Moore JS (1991) Functional instantiation in first-order logic. In: Lifschitz V (ed) Artificial intelligence and mathematical theory of computation: Papers in Honor of JohnMcCarthy, Academic Press, pp 7–26Google Scholar
- BH99.Brock, B., Hunt Jr., W.A.: Formal analysis of the motorola CAP DSP. Industrial-strength formal methods, pp. 81–115. Springer, Berlin (1999)CrossRefGoogle Scholar
- Ble71.Bledsoe, W.W.: Splitting and reduction heuristics in automatic theorem proving. Artif Intell
**2**, 55–77 (1971)CrossRefGoogle Scholar - BM72.Boyer RS, Moore JS (1972) The sharing of structure in theorem-proving programs. In: Machine intelligence 7, pp 101–116. Edinburgh University PressGoogle Scholar
- BM75.Boyer, R.S., Moore, J.S.: Proving theorems about pure lisp functions. JACM
**22**(1), 129–144 (1975)CrossRefGoogle Scholar - BM77.Boyer, R.S., Moore, J.S.: A fast string searching algorithm. Commun ACM
**20**(10), 762–772 (1977)CrossRefGoogle Scholar - BM79a.Boyer, R.S., Moore, J.S.: A computational logic. Academic Press, New York (1979)zbMATHGoogle Scholar
- BM79b.Boyer RS, Moore JS (1979) Metafunctions: proving them correct and using them efficiently as new proof procedures. Technical Report CSL-108, SRI InternationalGoogle Scholar
- BM81a.Boyer RS, Moore JS (1981) Metafunctions: proving them correct and using them efficiently as new proof procedures. In: The correctness problem in computer science. Academic Press, LondonGoogle Scholar
- BM81b.Boyer, R.S., Moore, J.S.: A verification condition generator for FORTRAN. The Correctness problem in computer science, pp. 9–101. Academic Press, London (1981)zbMATHGoogle Scholar
- BM82.Boyer RS, Moore JS (1982) On why it is impossible to prove that the BDX930 dispatcher implements a time-sharing system. In: Investigation, development, and evaluation of performance proving for fault-tolerant computer Final Report, covering the period September 1978 to June 1982, page Sections 14 and 15. Computer Science Laboratory, SRI International, Menlo Park, CAGoogle Scholar
- BM88a.Boyer, R., Moore, J.S.: The addition of bounded quantification and partial functions to a computational logic and its theorem prover. J Autom Reason
**4**(2), 117–172 (1988)MathSciNetCrossRefGoogle Scholar - BM88b.Boyer, R.S., Moore, J.S.: A computational logic handbook. Academic Press, New York (1988)zbMATHGoogle Scholar
- BM88c.Boyer RS, Moore JS (1988) Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic. In: Machine intelligence 11. Oxford University Press, pp 83–124Google Scholar
- BM97.Boyer, R.S., Moore, J.S.: A computational logic handbook, 2nd edn. Academic Press, New York (1997)zbMATHGoogle Scholar
- Boy71.Boyer, R.S.: Locking: a restriction of resolution. University of Texas at Austin, Department of Mathematics (1971)Google Scholar
- BP72.Burstall, R.M., Popplestone, R.J.: POP-2 reference manual. University of Edinburgh, Department of Machine Intelligence and Perception (1972)zbMATHGoogle Scholar
- BWAH06.Boyer RS, Hunt WA Jr (2006) Function memoization and unique object representation for ACL2 functions. In: ACL2 '06: proceedings of the sixth international workshop on the ACL2 theorem prover and its applications. ACM, New York, NY, USA, pp 81–89Google Scholar
- CDKM11.Chamarthis HR, Dillinger PC, Kaufmann M, Manolios P (2011) Integrating testing and interactive theorem proving. In: 10th international workshop on the ACL2 theorem prover and its applications, volume 70, pp 4–19. Electronic Proceedings in theoretical computer scienceCrossRefGoogle Scholar
- CDMV19.Chamarthi HR, Dillinger P, Manolios P, Vroon D (2019) The acl2 sedan. Technical report, Northeastern University, BostonGoogle Scholar
- CFHH+17.Cruz-Filipe L, Heule M, Hunt W, Kaufmann M, Schneider-Kamp P (2017) Efficient certified rat verification. In: 26th International conference on automated deduction (CADE 26). Springer, pp 220–236Google Scholar
- DFH+91.Dowek G, Felty A, Herbelin H, Huet G, Paulin C, Werner B (1991) The Coq proof assistant user's guide, Version 5.6. Technical Report TR 134, INRIAGoogle Scholar
- DM15.Davis, J., Myreen, M.: The reflective milawa theorem prover is sound (down to the machine code that runs it). J Autom Reason
**55**(2), 117–183 (2015)MathSciNetCrossRefGoogle Scholar - Gen69.Gentzen, G.: New version of the consistency proof for elementary number theory. In: Szabo, M.E. (ed.) The collected papers of Gerhard Gentzen, pp. 132–213. North-Holland Publishing Company, Amsterdam (1969)Google Scholar
- GM93.Gordon, M., Melham, T.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)zbMATHGoogle Scholar
- Goe16.Goel S (2016) Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. thesis, University of Texas at AustinGoogle Scholar
- GWAHK17.Goel Jr., S., Hunt, W.A., Kaufmann, M.: Engineering a formal, executable x86 ISA simulator for software verification, pp. 173–209. Springer, Berlin (2017)Google Scholar
- Hil99.Hiltzik, M.: Dealers of lightning: Xerox PARC and the dawn of the computer age. Harper Collins, New York (1999)Google Scholar
- HN00.Hickey, J., Nogin, A.: Fast tactic-based theorem proving. TPHOLs 2000, LNCS 1869, pp. 252–267. Springer, Heidelberg (2000)Google Scholar
- Hoa62.Hoare CAR (April 1962) Quicksort. Comput J 5(1):10–16Google Scholar
- Hod71.Hodes L (1971) Solving problems by formula manipulation. In: Proceedings of the Second international joint conference on artificial intelligence. British Computer Society, pp 553–559Google Scholar
- HSY06.Hardin DS, Smith EW, Young WD (2006) A robust machine code proof framework for highly secure applications. In: ACL2 '06: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications. ACM, New York, NY, USA, pp 11–20Google Scholar
- Hun10.Hunt W Jr (2010) Verifying VIA nano microprocessor components. In: Bloem R, Sharygina N (eds) FMCAD '10: Proceedings of the Formal methods in computer-aided design. ACM/IEEE, pp 3–10Google Scholar
- WAHKMS17.Hunt WA Jr, Kaufmann M, Moore JS, Slobodova A (2017) Industrial hardware and software verification with ACL2. In: Verified trustworthy software systems, volume 375. The Royal Society. (Article Number 20150399)CrossRefGoogle Scholar
- HWHKW17.Heule M Jr, Hunt W, Kaufmann M, Wetzler N (2017) Efficient, verified checking of propositional proofs. In: Interactive theorem proving (ITP) 2017, volume LNCS 10499. Springer, pp 269–284Google Scholar
- Kau88.Kaufmann M (1988) An interactive enhancement to the Boyer–Moore theorem prover. In: Proceedings of 9th international conference on automated deduction (CADE-9), volume LNCS 310. Springer, Berlin, pp 735–736Google Scholar
- Kau92.Kaufmann, M.: An extension to the Boyer-Moore theorem prover to support first-order quantification. J Autom Reason
**9**(3), 355–372 (1992)MathSciNetCrossRefGoogle Scholar - Kau18.Kaufmann M (2018) Defunt: a tool for automating termination proofs by using the community books (extended abstract). In: 15th International workshop on the ACL2 Theorem prover and its applications, volume 280, Electronic Proceedings in Theoretical Computer Science, pp 161–163CrossRefGoogle Scholar
- Kin69.King JC (1969) A program verifier. Ph.D. thesis, Carnegie-Mellon UniversityGoogle Scholar
- KK71.Ro, Kowalksi, Kuehner, D.: Linear resolution with selection function. Artif Intell
**2**, 227–260 (1971)MathSciNetCrossRefGoogle Scholar - KM18.Kaufmann M, Moore JS (2018) Limited second-order functionality in a first-order setting. J Autom ReasonGoogle Scholar
- KM19.Kaufmann M, Moore JS (2019) The ACL2 home page. In: http://www.cs.utexas.edu/users/moore/acl2/. Department of Computer Sciences, University of Texas at Austin
- KMM00a.Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-aided reasoning: ACL2 case studies. Kluwer Academic Press, Boston, MA (2000)Google Scholar
- KMM00b.Kaufmann, M., Manolios, P., Moore, J.S.: Computer-aided reasoning: an approach. Kluwer Academic Press, Boston, MA (2000)CrossRefGoogle Scholar
- Liu06.Liu H (2006) Formal Specification and verification of a JVM and its bytecode verifier. Ph.D. thesis, University of Texas at AustinGoogle Scholar
- Mac01.MacKenzie, D.: Mechanizing proof: computing, risk, and trust. MIT Press, Cambridge (2001)CrossRefGoogle Scholar
- McC63.McCarthy J (1963) A basis for a mathematical theory of computation. In: Computer programming and formal systems. North-Holland Publishing Company, AmsterdamCrossRefGoogle Scholar
- Mil79.Milner, R.: Lcf: a way of doing proofs with a machine. In: Jiří, Bečvář (ed.) Mathematical Foundations of Computer Science 1979. Lecture Notes in Computer Science, vol. 74, pp. 146–159. Springer, Berlin (1979)CrossRefGoogle Scholar
- Moo73.Moore JS (1973) Computational logic: structure sharing and proof of program properties. Ph.D. dissertation, University of Edinburgh. http://www.era.lib.ed.ac.uk/handle/1842/2245
- Moo75.Moore JS (1975) Automatic proof of the correctness of a binary addition algorithm. ACM SIGARG Newsl, pp 13–14Google Scholar
- Moo81.Moore JS (1981) Text editing primitives—the TXDT package. Technical Report CSL-81-2 (see http://www.cs.utexas.edu/users/moore/publications/txdt-package.pdf), Xerox PARC
- Moo15.Moore JS (2015) Stateman: using metafunctions to manage large terms representing machine states. In: ACL2 workshop 2015, volume 192, EPTCS, pp 93–109Google Scholar
- Moo17.Moore JS (2017) Computing verified machine address bounds during symbolic exploration of code. In: Provably correct systems, pp 151–172Google Scholar
- MV03.Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
**2741**, 243–257 (2003)zbMATHGoogle Scholar - NO79.Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans Program Lang
**1**, 245–257 (1979)CrossRefGoogle Scholar - NP92.Nipkow T, Paulson LC (1992) Isabelle-91. In: Kapur D (ed) Proceedings of the 11th international conference on automated deduction. Springer, Heidelberg LNAI 607. System abstract, pp 673–676CrossRefGoogle Scholar
- NWP02.Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle/HOL: a proof assistant for higher-order logic. Springer, Berlin (2002)CrossRefGoogle Scholar
- ORS92.Owre S, Rushby J, Shankar N (June 1992) PVS: a prototype verification system. In: Kapur D (ed) 11th International conference on automated deduction (CADE), Lecture Notes in Artificial Intelligence, Vol 607. Springer, Heidelberg, pp 748–752CrossRefGoogle Scholar
- PI17.Passmore GO, Ignatovich D (2017) Formal verification of financial algorithms. In: Conference on automated deduction (CADE 26), volume 10395. Springer LNCSGoogle Scholar
- Rob65.Robinson, J.A.: A machine-oriented logic based on the resolution principle. JACM
**12**(1), 23–41 (1965)MathSciNetCrossRefGoogle Scholar - Rus00.Russinoff DM (2000) A case study in formal verification of register-transfer logic with ACL2: the floating point adder of the AMD Athlon TM processor. In: Formal methods in computer-aided design (FMCAD 2000), volume LNCS 1954. SpringerGoogle Scholar
- Rus19.Russinoff, D.M.: Formal Verification of floating-point hardware design: a mathematical approach. Springer, Berlin (2019)CrossRefGoogle Scholar
- SDSWH11.Slobodova A, Davis J, Swords S Jr, Hunt W (2011) A flexible formal verification framework for industrial scale validation. In: Singh S (ed) 9th IEEE/ACM international conference on formal methods and models for codesign (MEMOCODE). IEEE, pp 89–97Google Scholar
- Sho79.Shostak, R.: A practical decision procedure for arithmetic with function symbols. JACM
**26**, 351–360 (1979)MathSciNetCrossRefGoogle Scholar - Ste90.Steele GL Jr (1990) Common Lisp the language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803Google Scholar
- Wan60.Wang, H.: Toward mechanical mathematics. IBM J Res Dev
**4**(1), 2–22 (1960)MathSciNetCrossRefGoogle Scholar - Wey80.Weyhrauch, R.: Prolegomena to a theory of mechanized formal reasoning. Artif Intell J
**13**(1), 133–170 (1980)MathSciNetCrossRefGoogle Scholar