The University of Texas at Austin ACL2 (A Computational Logic for Applicative Common Lisp)

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.

ACL2 is an interactive system in which you can model digital artifacts and guide the system to mathematical proofs about the behavior of those models. It has been used at such places as AMD, Centaur, IBM, and Rockwell Collins to verify interesting properties of commercial designs. It has been used to verify properties of models of microprocessors, microcode, the Sun Java Virtual Machine, operating system kernels, other verifiers, and interesting algorithms. For more details on the applications ACL2 has been used for see here

ACL2 is a mathematical logic together with a mechanical theorem prover to help you reason in the logic. The logic is just a subset of applicative Common Lisp. The theorem prover is an ``industrial strength'' version of the Boyer-Moore theorem prover, Nqthm. Models of all kinds of computing systems can be built in ACL2, just as in Nqthm, even though the formal logic is Lisp. Once you've built an ACL2 model of a system, you can run it. You can also use ACL2 to prove theorems about the model.

The logic of ACL2 is based on Common Lisp, however it formalizes only a subset of the language. It includes such familiar Lisp functions as cons, car and cdr for creating and manipulating list structures, various arithmetic primitives such as +, *, expt and <=, and intern and symbol-name for creating and manipulating symbols. Control primitives include cond, case and if, as well as function call, including recursion. New functions are defined with defun and macros with defmacro. See here for a list of the Common Lisp primitives supported by ACL2.

ACL2 supports five of Common Lisp's datatypes:

• the precisely represented, unbounded numbers (integers, rationals, and the complex numbers with rational components, called the "complex rationals" here)
• the characters with ASCII codes between 0 and 255
• strings of such characters
• symbols (including packages)
• conses

ACL2 is a very small subset of full Common Lisp. ACL2 does not include the Common Lisp Object System (CLOS), higher order functions, circular structures, and other aspects of Common Lisp that are non-applicative. Roughly speaking, a language is applicative if it follows the rules of function application. For example, f(x) must be equal to f(x), which means, among other things, that the value of f must not be affected by "global variables" and the object x must not change over time.

ACL2 is distributed on the Web without fee. There is a license agreement based on the 3-clause BSD license. See the file LICENSE in the ACL2 distribution. ACL2 currently runs on Unix, Linux, Windows, and Macintosh OS X operating systems. It can be built in any of the following Common Lisps:

• Allegro Common Lisp
• CCL (formerly OpenMCL)
• CLISP, CMU Common Lisp,
• GCL (Gnu Common Lisp), LispWorks, and
• SBCL (Steel Bank Common Lisp)

For more information about ACL2, see here.