FOM: ACL2 Tutorial Announcement

[Peter Manolios]

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

For the ACL2 workshop see
http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/ .

To register go to http://www-etaps.imag.fr/ .