- 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 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 ACL2-related resources.

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