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:
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.
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.
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.