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
- 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,
- 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