This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp
April 1997 (vol. 23 no. 4)
pp. 203-213

Abstract—ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's Pc-Nqthm, intended for large scale verification projects. This paper deals primarily with how we scaled up Nqthm's logic to an "industrial strength" programming language—namely, a large applicative subset of Common Lisp—while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola CAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on the AMD5K86 microprocessor by Advanced Micro Devices, Inc.

[1] R.L. Akers, "Strong Static Type Checking for Functional Common Lisp," PhD thesis, Univ. of Texas at Austin, 1993. Also available as Technical Report 96, Computational Logic, Inc., Suite 290, 1717 W. Sixth Street, Austin, Tex. URL http://www.cli.com/.
[2] K. Albin, "68020 Model Validation Testing," CLI Note 280, Aug. 1993.
[3] D. Basin and M. Kaufmann, "The Boyer-Moore Prover and Nuprl: An Experimental Comparison," Proc. First Workshop on "Logical Frameworks,"Antibes, France, May 1990.
[4] W.R. Bevier, W.A. Hunt, J. Strother Moore, and W.D. Young, "Special Issue on System Verification," J. Automated Reasoning, vol. 5, no. 4, pp. 409-530, 1989.
[5] W.R. Bevier and W.D. Young, "Machine Checked Proofs of the Design of a Fault-Tolerant Circuit," Formal Aspects of Computing, vol. 4, pp. 755-775, 1992. Also available as Technical Report 62, Computational Logic, Inc., Suite 290, 1717 West Sixth Street, Austin, Tex 78703, Aug., 1990 (URL http://www.cli.com/), and as NASA CR-182099, Nov.1990.
[6] R.S. Boyer, D. Goldschlag, M. Kaufmann, and J S. Moore, "Functional Instantiation in First Order Logic," Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7-26, Academic Press, 1991.
[7] R.S. Boyer, M. Kaufmann, and J S. Moore, "The Boyer-Moore Theorem Prover and Its Interactive Enhancement," Computers and Mathematics with Applications, vol. 29, no. 2, pp. 27-62, 1995.
[8] R.S. Boyer and J S. Moore, A Computational Logic.New York: Academic Press, 1979.
[9] R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
[10] R.S. Boyer and Y. Yu, "Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor," D. Kapur, ed., Automated Deduction-CADE-11, Lecture Notes in Computer Science 607 pp. 416-430, Springer-Verlag, 1992.
[11] R.K. Brayton, G.D. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S.-T. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R.K. Ranjan, S. Sarwary, T.R. Shiple, G. Swamy, and T. Villa, "VIS: A System for Verification and Synthesis," Proc. Eighth Int'l Conf. Computer-Aided Verification, July, 1996.
[12] B. Brock, M. Kaufmann, and J S. Moore, "ACL2 Theorems about Commercial Microprocessors," Formal Methods in Computer-Aided Design (FMCAD '96), M. Srivas and A. Camilleri, eds. , pp. 275-293. Springer-Verlag, Nov. 1996.
[13] S.-C. Chou, Mechanical Geometry Theorem Proving.Dordrecht, Holland: D. Reidel Publishing Co., 1988.
[14] E.M. Clarke and X. Zhao, "Analytica: A Theorem Prover for Mathematica," The J. of Mathematica, vol. 3, no. 1, pp. 56-71, Winter 1993.
[15] R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[16] C. Cornes, J. Courant, J.-C. Filliatre, G. Huet, and P. Manoury et al., "The Coq Proof Assistant, Reference Manual," Version 5.10. RT-0177, INRIA, B.P. 105, 78153 Le Chesnay Cedex, France.
[17] D. Craigen, S. Kromodimoeljo, I. Meisels, B. Pase, and M. Saaltink EVES: An Overview, "Odyssey Research Center," ORA Conf., Paper CP-91-5402-43, Mar. 1991.
[18] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS," Workshop on Industrial-Strength Formal Specification Techniques,Boca Raton, Fla., Apr. 1995. (http:// www.csl.sri.com/pvs.html)
[19] S. Gilfeather, J. Gehman, and C. Harrison, "Architecture of a Complex Arithmetic Processor for Communication Signal Processing," SPIE Proc., Int'l Symp. Optics, Imaging, and Instrumentation, 2296 Advanced Signal Processing: Algorithms, Architectures, and Implementations V, pp. 624-625, July, 1994.
[20] M.-J.-C. Gordon and T.-F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0-521-44189-7. Cambridge Univ. Press, 1993.
[21] W.M. Farmer, J.D. Guttman, and F.J. Thayer, "IMPS: An Interactive Mathematical Proof System," J. Automated Reasoning, vol. 11, no. 2, pp. 213-248, 1993.
[22] W.A. Hunt Jr. and B. Brock, "A Formal HDL and Its Use in the FM9001 Verification," Proc. Royal Society, 1992.
[23] M. Kaufmann, "A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover," Technical Report 19, Computational Logic, Inc., May, 1988. URL http://www.cli.com/
[24] M. Kaufmann and P. Pecchiari, "Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem," J. Automated Reasoning 16, nos. 1/2, pp. 181-222, 1996.
[25] M. Kaufmann and J S. Moore, "High-Level Correctness of ACL2: A Story (DRAFT)," Sept. 1995. URL ftp://ftp.cli.com/pub/ acl2/v1-8/acl2-sources/reports/story.txt
[26] K. Kunen, "A Ramsey Theorem in Boyer-Moore Logic," J. Automated Reasoning," vol. 15, no. 2, Oct. 1995.
[27] L. Lamport, "Types are Not Harmless," July, 1995. http:// www.research.digital.com/SRC/tla/tla.html
[28] W. McCune, "Otter 3.0 Reference Manual and Guide. Report ANl-94/6," Argonne National Lab., 1994.
[29] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[30] S.P. Miller and M. Srivas, "Formal Verification of the AAMP5 Microprocessor: A Case Study in the Industrial Use of Formal Methods," WIFT '95 Workshop on Industrial-Strength Formal Specification Techniques, Apr. 1995.
[31] J S. Moore, T. Lynch, and M. Kaufmann, "A MechanicallyChecked Proof of the Correctness of the Kernel of the AMD5K86 Floating Point Division Algorithm," Mar. 1996. URL http:// devil.ece.utexas.edu:80/lynch/divide/divide.html
[32] J S. Moorem, "A Formal Model of Asynchronous Communication and Its Use in Mechanically Verifying a Biphase Mark Protocol," Formal Aspects of Computing vol. 6, no. 1, pp. 60-91, 1994.
[33] J S. Moore, "Introduction to the OBDD Algorithm for the ATP Community," J. Automated Reasoning, vol. 12, pp. 33-45, 1994.
[34] L.C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science 828. Springer-Verlag, 1994.
[35] K.M. Pitman et al., draft proposed American National Standard for Information Systems—Programming Language--Common Lisp; X3J13/ 93-102. Global Eng. Documents, Inc., 1994.
[36] D.M. Russinoff, "A Mechanical Proof of Quadratic Reciprocity," J. Automated Reasoning, vol. 8, no. 1, pp. 3-21, 1992.
[37] D. Russinoff, "A Mechanically Checked Proof of Correctness of the AMD5K86 Floating-Point Square Root Microcode," Feb. 1997. http://www.onr.com/user/russ/david/fsqrt.html
[38] N. Shankar, Metamathematics, Machines, and Gödel's Proof. Cambridge Univ. Press, 1994.
[39] G.L. Steele Jr., Common LISP: The Language.Bedford, Mass.: Digital Press, 1984.
[40] G.L. Steele, Common Lisp: The Language, second ed. Digital Press, 1990.
[41] A. Trybulec, "Built-in Concepts," J. Formalized Mathematics, Axiomatics, 1989.
[42] W.D. Young, “Comparing Verification Systems: Interactive Consistency in ACL2,” IEEE Trans. Software Eng., vol. 23, no. 4, pp. 214–223 Apr. 1997

Index Terms:
Formal verification, automatic theorem proving, computational logic, partial functions, total functions, type checking, microcode verification, floating point division, digital signal processing.
Citation:
Matt Kaufmann, J S. Moore, "An Industrial Strength Theorem Prover for a Logic Based on Common Lisp," IEEE Transactions on Software Engineering, vol. 23, no. 4, pp. 203-213, April 1997, doi:10.1109/32.588534
Usage of this product signifies your acceptance of the Terms of Use.