ACL2 Tutorial

Presented by Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore

April 7, 2002, full day

Abstract :

ACL2 (``A Computational Logic for Applicative Common Lisp'') is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. We propose an ACL2 tutorial consisting of three parts:

  1. ACL2 Architecture and Overview We give an overview of the ACL2 system as a programming language, logic, and theorem prover. This includes a discussion of the various decision procedures and heuristics employed as well as advanced topics, including the efficient execution of models. We then give an overview of some applications of ACL2. This includes work on microprocessor modeling/analysis, on floating point verification, and on modeling/verification of Java byte code.

  2. The Flying Demo :This part of the tutorial gives a flavor of industrial-strength applications of ACL2 by going through some simple models and theorems, including bit vector manipulation algorithms, a netlist generator, a compiler, and Java Virtual Machine theorems. It also explains the role each of the various architectural components of the ACL2 theorem prover plays in the proof process.

  3. The Method Demo : Unlike the Flying Demo, here we go into one example in considerable detail, in order to illustrate how to interact successfully with ACL2. The main idea is to think about the high-level proof strategy and to look at the ``checkpoints'' of failed proofs for clues as to what to do next.