Milestones from the Pure Lisp Theorem Prover to ACL2. (English) Zbl 1427.68348

Moore, J Strother

Formal Asp. Comput. 31, No. 6, 699-732 (2019).

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:

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

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 1494.68284
[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 1483.68483
[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