Proving Theorems about Commercial Microprocessors: Recent Results with ACL2

Abstract

ACL2 is an interactive mechanical theorem prover designed for use in modeling hardware and software and proving properties about those models. ACL2 stands for ``A Computational Logic for Applicative Common Lisp.'' It has been used to prove theorems about a variety of algorithms and designs, including floating-point division and square root on both the AMD K5 (where the operations are done in microcode) and K7 (where they are done using different algorithms in hardware). ACL2 has also been used in microprocessor modeling, including the Motorola CAP DSP chip and the Rockwell- Collins JEM1 Java Virtual Machine microprocessor. In this talk I discuss ACL2 and some of its recent applications.

• http://www.cs.utexas.edu/users/moore/publications/bkm96.ps.Z ACL2 Theorems about Commercial Microprocessors, B. Brock, M. Kaufmann and J S. Moore. In M. Srivas and A. Camilleri (eds.) Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96), Springer-Verlag, pp. 275-293, 1996.
• http://www.cs.utexas.edu/users/moore/publications/km97.ps.Z An Industrial Strength Theorem Prover for a Logic Based on Common Lisp, M. Kaufmann and J S. Moore, IEEE Transactions on Software Engineering 23(4), April 1997, pp. 203-213.
• http://www.cs.utexas.edu/users/boyer/bm96.ps.Z Mechanized Formal Reasoning about Programs and Computing Machines, R. S. Boyer and J S. Moore. In R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996.