FOM: ACL2 Tutorial Announcement
pete at cs.utexas.edu
Tue Feb 19 10:53:57 EST 2002
An ACL2 tutorial will be held on April 7, 2002 in Grenoble, France, as
part of ETAPS 2002 (and immediately preceding the ACL2 Workshop, also at ETAPS
2000). 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 see
For the ACL2 workshop see
To register go to http://www-etaps.imag.fr/ .
More information about the FOM