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 a 3-clause BSD license),
as are many papers about ACL2 and its applications.
In addition, the page links to many other books and papers and other