Advertisement

Towards a Mechanically Checked Theory of Computation

The ACL2 Project
  • J Strother Moore
Chapter
  • 378 Downloads
Part of the The Springer International Series in Engineering and Computer Science book series (SECS, volume 597)

Abstract

Formal mathematical logic is ideally suited to describing computational processes. We discuss the use of one particular mechanized mathematical logic, namely ACL2 (A Computational Logic for Applicative Common Lisp) to model computational problems and to prove theorems about such models. After a few elementary examples, we explain how computational artifacts are formalized in ACL2 and we summarize the main industrial applications of ACL2 as of 1999.

Keywords

Automatic theorem proving hardware verification software verification 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Boyer, R., Goldschlag, D., Kaufmann, M., and Moore, J. S. (1991). Functional instantiation in first-order logic. In Lifschitz, V., editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 7–26. Academic Press.Google Scholar
  2. Boyer, R. S. and Moore, J. S. (1975). Proving theorems about pure lisp functions. JACM, 22(1):129–144.MathSciNetzbMATHCrossRefGoogle Scholar
  3. Boyer, R. S. and Moore, J. S. (1979). A Computational Logic. Academic Press, New York.zbMATHGoogle Scholar
  4. Boyer, R. S. and Moore, J. S. (1996). Mechanized formal reasoning about programs and computing machines. In Veroff, R., editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, pages 147–176. MIT Press.Google Scholar
  5. Boyer, R. S. and Moore, J. S. (1997). A Computational Logic Handbook, Second Edition. Academic Press, New York.Google Scholar
  6. Boyer, R. S. and Moore, J. S. (1999). Single-threaded objects in ACL2. (submitted for publication).Google Scholar
  7. Brock, B., Kaufmann, M., and Moore, J. S. (1996). ACL2 theorems about commercial microprocessors. In Srivas, M. and Camilleri, A., editors, Formal Methods in Computer-Aided Design (FMCAD′96), pages 275–293. Springer-Verlag, LNCS 1166.Google Scholar
  8. Brock, B. and Moore, J. S. (1999). A mechanically checked proof of a comparator sort algorithm, (submitted for publication).Google Scholar
  9. Bryant, R. (1992). Symbolic boolean manipulation with ordered binary decision diagrams. Technical Report CMU-CS-92-160, School of Computer Science, Carnegie Mellon University.Google Scholar
  10. Cohen, R. M. (1997). The defensive Java Virtual Machine specification, version 0.53. Technical report, Electronic Data Systems Corp, Austin Technical Services Center, 98 San Jacinto Blvd, Suite 500, Austin, TX 78701.Google Scholar
  11. Goodstein, R. L. (1964). Recursive Number Theory. North-Holland Publishing Company, Amsterdam.Google Scholar
  12. Gordon, M. and Melham, T. (1993). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press.Google Scholar
  13. Greve, D. A. (1998). Symbolic simulation of the JEM1 microprocessor. Technical Report (submitted), Advanced Technology Center, Rockwell Collins, Inc., Cedar Rapids, IA 52498.Google Scholar
  14. Greve, D. A. and Wilding, M. M. (Jan. 12, 1998). Stack-based Java a back-to-future step. Electronic Engineering Times, page 92.Google Scholar
  15. Kaufmann, M. (1998). ACL2 support for verification projects. In Kirchner, C. and Kirchner, H., editors, Proceedings 15th International Conference on Automated Deduction, pages 220–238. LNAI 1421, Springer-Verlag.Google Scholar
  16. Kaufmann, M., Manolios, P., and Moore, J. S. (2000). ACL2: A Tutorial Introduction. Kluwer.Google Scholar
  17. Kaufmann, M. and Moore, J. S. (1997). An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203–213.CrossRefGoogle Scholar
  18. Kaufmann, M. and Moore, J. S. (1999a). The ACL2 User’s Manual http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html.Google Scholar
  19. Kaufmann, M. and Moore, J. S. (1999b). Structured theory development for a mechanized logic, (submitted for publication).Google Scholar
  20. Lindholm, T. and Yellin, F. (1996). The Java Virtual Machine Specification. Addison-Wesley.Google Scholar
  21. Manolios, P., Namjoshi, K., and Sumners, R. (1999). Linking theorem proving and model-checking with well-founded bisimulation. In Computed Aided Verification, CAV ′99, pages 369–379. Springer-Verlag LNCS 1633.Google Scholar
  22. McCarthy, J. (1959). Programs with common sense. In Proceedings of the Teddington Conference on the Mechanization of Thought Processes, pages 75–91. H.M.Stationery Office.Google Scholar
  23. McCarthy, J. (1962). Towards a mathematical science of computation. In Proceedings of IFIP Congress, pages 21–28. North-Holland.Google Scholar
  24. McCarthy, J. (1963). A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, pages 33–70. North-Holland Publishing Company, Amsterdam, The Netherlands.CrossRefGoogle Scholar
  25. McCune, W. (1994). Otter 3.0 Reference Manual and Guide. Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL. See also URL http://www.mcs.anl.gov/AR/otter/.CrossRefGoogle Scholar
  26. Moore, J. S. (1994). Introduction to the OBDD algorithm for the ATP community. Journal of Automated Reasoning, 12(1):33–45.MathSciNetzbMATHCrossRefGoogle Scholar
  27. Moore, J. S. (1999a). A mechanically checked proof of a multiprocessor result via a uniprocessor view. Formal Methods in System Design, 14(2):213–228.CrossRefGoogle Scholar
  28. Moore, J. S. (1999b). Proving theorems about Java-like byte code. In Olderog, E.-R. and Steffen, B., editors, Correct System Design — Recent Insights and Advances, pages 139–162. LNCS 1710.Google Scholar
  29. Moore, J. S., Lynch, T., and Kaufmann, M. (1998). A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Transactions on Computers, 47(9):913–926.MathSciNetCrossRefGoogle Scholar
  30. Owre, S., Rushby, J., and Shankar, N. (1992). PVS: A prototype verification system. In Kapur, D., editor, 11th International Conference on Automated Deduction (CADE), pages 748–752. Lecture Notes in Artificial Intelligence, Vol 607, Springer-Verlag.Google Scholar
  31. Russinoff, D. M. (1998). A mechanically checked proof of IEEE compliance of the floating point multiplication, division, and square root algorithms of the AMD-K7 processor, http://www.onr.com/user/russ/david/k7-div-sqrt.html.Google Scholar
  32. Sawada, J. and Hunt, W. (1998). Processor verification with precise exceptions and speculative execution. In Computed Aided Verification, CAV ′98, pages 135–146. Springer-Verlag LNCS 1427.Google Scholar
  33. Shoenfield, J. R. (1967). Mathematical Logic. Addison-Wesley, Reading, Ma.zbMATHGoogle Scholar
  34. Smith, S. W. and Austel, V. (1998). Trusting trusted hardware: Towards a formal model for programmable secure coprocessors. In Proceedings of the Third USENIX Workshop on Electronic Commerce, pages 83–98.Google Scholar
  35. Standards Committee of the IEEE Computer Society (1985). IEEE standard for binary floating-point arithmetic. Technical Report IEEE Std. 754–1985, IEEE, 345 East 47th Street, New York, NY 10017.Google Scholar
  36. Steele, Jr., G. L. (1990). Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803.zbMATHGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • J Strother Moore
    • 1
  1. 1.Department of Computer SciencesUniversity of TexasAustinUSA

Personalised recommendations