ACL2 Version 2.5 News

We will give an ACL2 tutorial at the CADE18/FLoC conference in Copenhagen this summer (July, 2002).

Two books about ACL2 have appeared in June, 2000! Find out more about them here. Kluwer has given us permission to post this order form for the books that provides a 25% discount.

The ACL2 Workshop will be held this year in Austin, October 29-31, 2000, just before FMCAD.

Check out the HTML versions of two ACL2 demos.

The first is a talk, usually given with a laptop, in which ACL2 is used to prove insertion sort, some bit vector manipulation algorithms, a netlist generator, a compiler, and some Java Virtual Machine theorems. You can see why it's called the Flying Demo. In a way, the Flying Demo is just an advertisement for ACL2, but instead of showing you industrial-strength models and theorems it shows you simple ones that are suggestive of more interesting applications.

The second demo is a Tutorial on how to interact with ACL2 to find proofs. The Tutorial illustrates what we call ``The Method,'' which consists mainly of thinking and looking at the checkpoints of failed proofs for clues as to what to do next.

If you have comments about or corrections to either of these HTML demos, please contact and

Here are the postscript slides (1.5MB) for a talk on ACL2 given at the AAAI-2000 meeting in Austin, Texas (August, 2000).