FOM: ACL2 Tutorial in Copenhagen
pete at cs.utexas.edu
Sat Jun 15 13:41:01 EDT 2002
A tutorial on ACL2 will be held on July 25, 2002 in Copenhagen, Denmark, as
part of CADE18, which is part of FloC 2002. The organizers are:
Matt Kaufmann (Advanced Micro Devices, Inc.)
Panagiotis (Pete) Manolios (Georgia Institute of Technology)
J Strother Moore (University of Texas at Austin)
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.
ACL2 architecture and applications
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.
The Flying Demo
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.
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.
For more information about the tutorial see
The CADE Web page is http://floc02.diku.dk/CADE/ .
The FLoC Web page is http://floc02.diku.dk/ .
To register go to http://floc02.diku.dk/floc/register.html .
More information about the FOM