
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
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. 203213, April, 1997.  
BibTex  x  
@article{ 10.1109/32.588534, author = {Matt Kaufmann and J S. Moore}, title = {An Industrial Strength Theorem Prover for a Logic Based on Common Lisp}, journal ={IEEE Transactions on Software Engineering}, volume = {23}, number = {4}, issn = {00985589}, year = {1997}, pages = {203213}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.588534}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  An Industrial Strength Theorem Prover for a Logic Based on Common Lisp IS  4 SN  00985589 SP203 EP213 EPD  203213 A1  Matt Kaufmann, A1  J S. Moore, PY  1997 KW  Formal verification KW  automatic theorem proving KW  computational logic KW  partial functions KW  total functions KW  type checking KW  microcode verification KW  floating point division KW  digital signal processing. VL  23 JA  IEEE Transactions on Software Engineering ER   
Abstract—ACL2 is a reimplemented extended version of Boyer and Moore's Nqthm and Kaufmann's PcNqthm, 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 AMD5_{K}86 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 BoyerMoore 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. 409530, 1989.
[5] W.R. Bevier and W.D. Young, "Machine Checked Proofs of the Design of a FaultTolerant Circuit," Formal Aspects of Computing, vol. 4, pp. 755775, 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 CR182099, 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. 726, Academic Press, 1991.
[7] R.S. Boyer, M. Kaufmann, and J S. Moore, "The BoyerMoore Theorem Prover and Its Interactive Enhancement," Computers and Mathematics with Applications, vol. 29, no. 2, pp. 2762, 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 DeductionCADE11, Lecture Notes in Computer Science 607 pp. 416430, SpringerVerlag, 1992.
[11] R.K. Brayton, G.D. Hachtel, A. SangiovanniVincentelli, 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. ComputerAided Verification, July, 1996.
[12] B. Brock, M. Kaufmann, and J S. Moore, "ACL2 Theorems about Commercial Microprocessors," Formal Methods in ComputerAided Design (FMCAD '96), M. Srivas and A. Camilleri, eds. , pp. 275293. SpringerVerlag, 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. 5671, 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. RT0177, 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 CP91540243, Mar. 1991.
[18] J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas, "A Tutorial Introduction to PVS," Workshop on IndustrialStrength 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. 624625, July, 1994.
[20] M.J.C. Gordon and T.F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. ISBN 0521441897. 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. 213248, 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 BoyerMoore Theorem Prover," Technical Report 19, Computational Logic, Inc., May, 1988. URL http://www.cli.com/
[24] M. Kaufmann and P. Pecchiari, "Interaction with the BoyerMoore Theorem Prover: A Tutorial Study Using the ArithmeticGeometric Mean Theorem," J. Automated Reasoning 16, nos. 1/2, pp. 181222, 1996.
[25] M. Kaufmann and J S. Moore, "HighLevel Correctness of ACL2: A Story (DRAFT)," Sept. 1995. URL ftp://ftp.cli.com/pub/ acl2/v18/acl2sources/reports/story.txt
[26] K. Kunen, "A Ramsey Theorem in BoyerMoore 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 ANl94/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 IndustrialStrength 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. 6091, 1994.
[33] J S. Moore, "Introduction to the OBDD Algorithm for the ATP Community," J. Automated Reasoning, vol. 12, pp. 3345, 1994.
[34] L.C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science 828. SpringerVerlag, 1994.
[35] K.M. Pitman et al., draft proposed American National Standard for Information Systems—Programming LanguageCommon Lisp; X3J13/ 93102. Global Eng. Documents, Inc., 1994.
[36] D.M. Russinoff, "A Mechanical Proof of Quadratic Reciprocity," J. Automated Reasoning, vol. 8, no. 1, pp. 321, 1992.
[37] D. Russinoff, "A Mechanically Checked Proof of Correctness of the AMD5K86 FloatingPoint 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, "Builtin 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