Milestones from the Pure Lisp Theorem Prover to ACL2.

*(English)*Zbl 1427.68348Summary: We discuss the evolutionary path from the Edinburgh Pure Lisp Theorem Prover of the early 1970s to its modern counterpart, A Computational Logic for Applicative Common Lisp, 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.

##### MSC:

68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |

68-03 | History of computer science |

##### Keywords:

theorem proving; hardware; software; verification; functional programming; Lisp; induction; rewriting; reflection; decision procedures##### Software:

Isabelle/HOL; LISP; HOL; ACL2; Coq; LCF; PVS; Jitawa; ML ; NQTHM; TXDT; Milawa; Quicksort; DefunT
PDF
BibTeX
XML
Cite

\textit{J. S. Moore}, Formal Asp. Comput. 31, No. 6, 699--732 (2019; Zbl 1427.68348)

Full Text:
DOI

**OpenURL**

##### References:

[1] | Bledsoe, Ww; Bruell, P., A man-machine theorem-proving system, Artif Intell, 5, 51-72 (1974) · Zbl 0286.68047 |

[2] | Boyer RS, Davies DJM, Moore JS (1973) The 77-editor. Technical Report 62, Department of Computational Logic, University of Edinburgh |

[3] | 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-26 |

[4] | Brock, B.; Hunt, Wa Jr, Formal analysis of the motorola CAP DSP, Industrial-strength formal methods, 81-115 (1999), Berlin: Springer, Berlin |

[5] | Bledsoe, Ww, Splitting and reduction heuristics in automatic theorem proving, Artif Intell, 2, 55-77 (1971) · Zbl 0221.68052 |

[6] | Boyer RS, Moore JS (1972) The sharing of structure in theorem-proving programs. In: Machine intelligence 7, pp 101-116. Edinburgh University Press |

[7] | Boyer, Rs; Moore, Js, Proving theorems about pure lisp functions, JACM, 22, 1, 129-144 (1975) · Zbl 0338.68014 |

[8] | Boyer, Rs; Moore, Js, A fast string searching algorithm, Commun ACM, 20, 10, 762-772 (1977) · Zbl 1219.68165 |

[9] | Boyer, Rs; Moore, Js, A computational logic (1979), New York: Academic Press, New York |

[10] | Boyer RS, Moore JS (1979) Metafunctions: proving them correct and using them efficiently as new proof procedures. Technical Report CSL-108, SRI International |

[11] | 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, London |

[12] | Boyer, Rs; Moore, Js, A verification condition generator for FORTRAN, The Correctness problem in computer science, 9-101 (1981), London: Academic Press, London |

[13] | 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, CA |

[14] | Boyer, R.; Moore, Js, The addition of bounded quantification and partial functions to a computational logic and its theorem prover, J Autom Reason, 4, 2, 117-172 (1988) · Zbl 0653.03007 |

[15] | Boyer, Rs; Moore, Js, A computational logic handbook (1988), New York: Academic Press, New York |

[16] | 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-124 |

[17] | Boyer, Rs; Moore, Js, A computational logic handbook (1997), New York: Academic Press, New York |

[18] | Boyer, Rs, Locking: a restriction of resolution (1971), Department of Mathematics: University of Texas at Austin, Department of Mathematics |

[19] | Burstall, Rm; Popplestone, Rj, POP-2 reference manual (1972), Department of Machine Intelligence and Perception: University of Edinburgh, Department of Machine Intelligence and Perception |

[20] | 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-89 |

[21] | Chamarthi, Harsh Raju; Dillinger, Peter C.; Kaufmann, Matt; Manolios, Panagiotis, Integrating Testing and Interactive Theorem Proving, Electronic Proceedings in Theoretical Computer Science, 70, 4-19 (2011) |

[22] | Chamarthi HR, Dillinger P, Manolios P, Vroon D (2019) The acl2 sedan. Technical report, Northeastern University, Boston · Zbl 1316.68132 |

[23] | 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-236 · Zbl 06778406 |

[24] | 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, INRIA |

[25] | 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) · Zbl 1356.68186 |

[26] | Gentzen, G.; Szabo, Me, New version of the consistency proof for elementary number theory, The collected papers of Gerhard Gentzen, 132-213 (1969), Amsterdam: North-Holland Publishing Company, Amsterdam |

[27] | Gordon, M.; Melham, T., Introduction to HOL: a theorem proving environment for higher order logic (1993), Cambridge: Cambridge University Press, Cambridge · Zbl 0779.68007 |

[28] | Goel S (2016) Formal verification of application and system programs based on a validated x86 ISA model. Ph.D. thesis, University of Texas at Austin |

[29] | Goel, S. Jr; Hunt, Wa; Kaufmann, M., Engineering a formal, executable x86 ISA simulator for software verification, 173-209 (2017), Berlin: Springer, Berlin |

[30] | Hiltzik, M., Dealers of lightning: Xerox PARC and the dawn of the computer age (1999), New York: Harper Collins, New York |

[31] | Hickey, J.; Nogin, A., Fast tactic-based theorem proving, TPHOLs 2000, LNCS 1869, 252-267 (2000), Heidelberg: Springer, Heidelberg · Zbl 0974.68534 |

[32] | Hoare CAR (April 1962) Quicksort. Comput J 5(1):10-16 |

[33] | Hodes L (1971) Solving problems by formula manipulation. In: Proceedings of the Second international joint conference on artificial intelligence. British Computer Society, pp 553-559 |

[34] | 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-20 |

[35] | 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-10 |

[36] | Hunt, Warren A.; Kaufmann, Matt; Moore, J. Strother; Slobodova, Anna, Industrial hardware and software verification with ACL2, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375, 2104, 20150399 (2017) |

[37] | 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-284 · Zbl 06821857 |

[38] | 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-736 |

[39] | Kaufmann, M., An extension to the Boyer-Moore theorem prover to support first-order quantification, J Autom Reason, 9, 3, 355-372 (1992) · Zbl 0784.68076 |

[40] | Kaufmann, Matt, DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract), Electronic Proceedings in Theoretical Computer Science, 280, 161-163 (2018) |

[41] | King JC (1969) A program verifier. Ph.D. thesis, Carnegie-Mellon University |

[42] | Ro, Kowalksi; Kuehner, D., Linear resolution with selection function, Artif Intell, 2, 227-260 (1971) · Zbl 0234.68037 |

[43] | Kaufmann M, Moore JS (2018) Limited second-order functionality in a first-order setting. J Autom Reason |

[44] | 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 |

[45] | Kaufmann, M.; Manolios, P.; Moore, Js, Computer-aided reasoning: ACL2 case studies (2000), Boston, MA: Kluwer Academic Press, Boston, MA |

[46] | Kaufmann, M.; Manolios, P.; Moore, Js, Computer-aided reasoning: an approach (2000), Boston, MA: Kluwer Academic Press, Boston, MA |

[47] | Liu H (2006) Formal Specification and verification of a JVM and its bytecode verifier. Ph.D. thesis, University of Texas at Austin |

[48] | Mackenzie, D., Mechanizing proof: computing, risk, and trust (2001), Cambridge: MIT Press, Cambridge · Zbl 1063.68500 |

[49] | Mccarthy, John, A Basis for a Mathematical Theory of Computation), Computer Programming and Formal Systems, 33-70 (1963) · Zbl 0203.16402 |

[50] | Milner, R.; Jiří, Bečvář, Lcf: a way of doing proofs with a machine, Mathematical Foundations of Computer Science 1979, 146-159 (1979), Berlin: Springer, Berlin |

[51] | 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 |

[52] | Moore JS (1975) Automatic proof of the correctness of a binary addition algorithm. ACM SIGARG Newsl, pp 13-14 |

[53] | 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 |

[54] | Moore JS (2015) Stateman: using metafunctions to manage large terms representing machine states. In: ACL2 workshop 2015, volume 192, EPTCS, pp 93-109 |

[55] | Moore JS (2017) Computing verified machine address bounds during symbolic exploration of code. In: Provably correct systems, pp 151-172 |

[56] | Manolios, P.; Vroon, D., Algorithms for ordinal arithmetic, Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), 2741, 243-257 (2003) · Zbl 1278.68272 |

[57] | Nelson, G.; Oppen, Dc, Simplification by cooperating decision procedures, ACM Trans Program Lang, 1, 245-257 (1979) · Zbl 0452.68013 |

[58] | Nipkow, Tobias; Paulson, Lawrence C., Isabelle-91, Automated Deduction—CADE-11, 673-676 (1992), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg |

[59] | Nipkow, T.; Wenzel, M.; Paulson, Lc, Isabelle/HOL: a proof assistant for higher-order logic (2002), Berlin: Springer, Berlin · Zbl 0994.68131 |

[60] | Owre, S.; Rushby, J. M.; Shankar, N., PVS: A prototype verification system, Automated Deduction—CADE-11, 748-752 (1992), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg |

[61] | Passmore GO, Ignatovich D (2017) Formal verification of financial algorithms. In: Conference on automated deduction (CADE 26), volume 10395. Springer LNCS |

[62] | Robinson, Ja, A machine-oriented logic based on the resolution principle, JACM, 12, 1, 23-41 (1965) · Zbl 0139.12303 |

[63] | 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. Springer |

[64] | Russinoff, Dm, Formal Verification of floating-point hardware design: a mathematical approach (2019), Berlin: Springer, Berlin |

[65] | 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-97 |

[66] | Shostak, R., A practical decision procedure for arithmetic with function symbols, JACM, 26, 351-360 (1979) · Zbl 0496.03003 |

[67] | Steele GL Jr (1990) Common Lisp the language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803 |

[68] | Wang, H., Toward mechanical mathematics, IBM J Res Dev, 4, 1, 2-22 (1960) · Zbl 0097.00404 |

[69] | Weyhrauch, R., Prolegomena to a theory of mechanized formal reasoning, Artif Intell J, 13, 1, 133-170 (1980) · Zbl 0435.68070 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.