This one day tutorial is part of
CADE18, which is part of FloC
2002 and will be held in Copenhagen, Denmark, on July 25 2002.
Tutorial Description
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.
The ACL2 tutorial consists of three parts:
- ACL2 architecture and applications: Overview of ACL2 and how it
is used.
- The Flying Demo: Some illustrative applications of ACL2.
- The Method Demo: How to use ACL2.
We give an overview of the ACL2 system. We
describe the programming language, its relation to Common Lisp, and
how it is implemented. We present aspects of the logic and give an
overview of the architecture of the theorem prover. This includes a
discussion of the various decision procedures and heuristics
employed. We also touch on advanced topics, e.g., the efficient
execution of models. The final component of this part is an overview
of the applications of ACL2. This includes work on microprocessor
modeling/analysis, on floating point verification, and on
modeling/verification of Java byte code.
We show how to use ACL2 to prove insertion sort, some bit vector
manipulation algorithms, a netlist generator, a compiler, and some
Java Virtual Machine theorems. This part of the tutorial gives a
flavor of industrial-strength applications of ACL2 by going through
some simple models and theorems. It also explains the role each of
the various architectural components of the ACL2 theorem prover plays
in the proof process.
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.
References
Previous workshops and tutorials:
The first workshop resulted in the following book:
In addition, the following book is a textbook introduction to ACL2.
