ACL2

ACL2 (A Computational Logic for Applicative Common Lisp) is a theorem prover for industrial Applications. It is both a mathematical logic and a system of tools for constructing proofs in the logic.

This system is intended for specifying and proving properties of computing machines. It has also been used in several projects (some described here). A listing of publications about ACL2 can be found here.) for modeling and proving properties of commercial microprocessor products by Motorola, AMD, Rockwell Collins, and IBM.

ACL2 works with GCL, CMUCL, CLISP and a number of commercial Common Lisp systems. Source code distributed under the terms of the GPL, and a lot of documentation, are available at the project page.

It can be used with a web interface: proof-pad.

---

Theorem Provers

Account name Password

register