A Computational Logic for Applicative Common Lisp (ACL2)

ACL2 is a direct descendent of the Boyer-Moore theorem prover, intended for large scale verification projects. ACL2 was created by Matt Kaufmann and J Moore, working from a kernel developed by Boyer and Moore. The key ideas in ACL2 are

The logic supported by the theorem prover is (an extension of a subset of) applicative Common Lisp.
The system is coded in its own logic.
The system supports incremental and collaborative proof projects.

I think it's really cool that the system is coded in its own logic. How many theorem provers can you say that about? How many 5 Mbyte applicative programs can you name?

ACL2 is quite young by Nqthm's standards. (The ACL2 Project was begun in 1989.) But it has been used to do some impressive things.

the IEEE compliance of the hardware implementing the elementary floating point operations on the AMD Athlon microprocessor (Russinoff and Flatau, of AMD),
an executable model of the Rockwell-Collins JEM1, the world's first silicon Java Virtual Machine (Hardin, Greve, and Wilding, of Rockwell-Collins),
the security model and a formal analysis of the bootstrapping code for the IBM 4758 secure coprocessor (Austel and Smith, of IBM),
the correctness of a safety-critical compiler ``checker'' for trainborne control software by Union Switch and Signal (Bertoli and Traverso, of IRST, Italy), and
a model of and theorems about the Motorola CAP digital signal processor (Bishop Brock, then of CLI) including:
- a bit- and cycle-accurate CAP model that runs several times faster than the SPW model
- the correctness of a function that detects pipeline hazards in CAP microcode, and
- the correctness of several CAP microcode programs.

The comprehensive source for information about ACL2 is the ACL2 Home Page. Sources and documentation are freely distributed from there (under the GNU General Public License), as are many papers about ACL2 and its applications. In addition, the page links to many other books and papers and other ACL2-related resources.

[Best Ideas] [Publications] [Research] [Home]