FOM: ACL2 Tutorial in Copenhagen

[Peter Manolios]

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
http://www.cc.gatech.edu/~manolios/acl2-cade-tutorial.html .

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 .