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. (In particular, this includes a demo of the interactive `verify' loop sometimes called the ``proof-checker''.
The third demo is really a collection of demos. They form the basis of a one-hour talk given at TPHOLs in August, 2008. A gzipped tarfile includes all files on the web page for these demos.
The fourth demo illustrates both high-level strategy and lower-level
tactics. It is available as a gzipped tarfile or as a directory on the web. Start
with the README file.
If you have comments about or corrections to any of these demos, please contact kaufmann@cs.utexas.edu and moore@cs.utexas.edu.
On a related note: Here are the postscript slides (1.5MB) for a talk on ACL2 given at the AAAI-2000 meeting in Austin, Texas (August, 2000). Also of possible interest: Matt Kaufmann's presentation at UITP 2008.