Proving Theorems about Commercial Microprocessors: Recent Results with ACL2
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.
Please see the ACL2 home page http://www.cs.utexas.edu/users/moore/acl2. Especially relevant are the three papers.
Slides in postscript available here.