Third International Workshop on the ACL2 Theorem Prover
and Its Applications (ACL2-2002)

Affiliated with
ETAPS 2002


ACL2-2002 was held on April 8-9 (Monday/Tuesday), 2002, in Grenoble, France. This workshop was a satellite event of ETAPS 2002. An ACL2 tutorial took place on April 7, the day before the workshop. See its tutorial web page for more information.

Jun Sawada has kindly provided pictures (click here).

ACL2 is a state-of-the-art automated reasoning system, which grew out of the Boyer-Moore theorem prover and has been used successfully on a number of industrial and academic projects. ACL2 is described at

The ACL2 workshops provides a forum for presentation and discussion of projects using ACL2 as well as evolution of the tool. The first workshop was held at the University of Texas in March 1999, resulting in two books:

The second workshop was held in October 2000, resulting in on-line proceedings.

Other conferences and workshops at ETAPS 2002. may be of interest to the ACL2 community. In particular, Designing Correct Circuits was held on on April 6-7, 2002 (immediately before the ACL2 workshop).

Papers were refereed by members of the Program Committee.


Sunday, April 7:
Full-Day ACL2 Tutorial
(separate registration required)
Monday, April 8:
Workshop, Day 1
9:00 ETAPS Welcome
9:30 ETAPS Invited Talk: Greg Morrisett, Type Checking Systems Code
10:45   Coffee break
11:15   ACL2 Welcome
11:25 D. Borrione,
P. Georgelin,
P. Ostier
A Framework for VHDL Combining Theorem Proving and Symbolic Simulation
[PDF] [PS] [Supporting materials]
11:55 J. L. Caldwell,
J. R. Cowles
Representing Nuprl Proof Objects in ACL2: toward a proof checker for Nuprl
[PDF] [PS]
12:15 J. Sawada Formal Verification of Divide and Square Root Algorithms Using Series Calculation
[PDF] [PS]
12:45   Lunch
14:15 R. A. Gamboa,
B. E. Middleton
Taylor's Formula with Remainder
[PDF] [PS]
14:45 I. Medina-Bulo,
F. Palomo-Lozano,
J. A. Alonso-Jiménez
Implementation in ACL2 of Well-Founded Polynomial Orderings
[PDF] [PS] [Supporting materials]
15:05   Short break
15:25 J.-L. Ruiz-Reina,
J.-A. Alonso,
M.-J. Hidalgo,
F.J. Martín-Mateos
A Theory About First-order Terms in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PS] [PDF])
15:55 J.-L. Ruiz-Reina,
J.-A. Alonso,
M.-J. Hidalgo,
F.J. Martín-Mateos
Progress Report: Term Dags Using Stobjs
[PDF] [PS] [Supporting materials] (Slides: [PS] [PDF])
16:15   Coffee break
16:45 P. Manolios,
M. Kaufmann
Adding a Total Order to ACL2
[PDF] [PS] [Supporting materials]
17:15 M. Kaufmann,
J Moore
What's New in ACL2?
[PDF] [PS] (Slides: [PS] [PDF])
17:55   Discussion
18:45   End of Day 1
Tuesday, April 9:
Workshop, Day 2
9:00 ETAPS Invited Talk: Hellmuth Broda, Jini Software Architecture - The end of Protocols as we know them
10:00   Coffee break
10:45 R. Sumners Checking ACL2 Theorems via SAT Checking
[PDF] [PS] (Slides: [PS] [PDF])
11:15 M. Kaufmann,
R. Sumners
Efficient Rewriting of Data Structures in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PS] [PDF])
11:35   Short break
11:55 J. Cowles Consistently Adding Primitive Recursive Definitions in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PDF])
12:15 J. Cowles Flat Domains and Recursive Equations in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PDF])
12:45   Lunch
14:15 ETAPS Invited Talk: Michael Lowry, Software Construction and Analysis Tools for Future Space Missions
15:15   Coffee break
16:00 F.J. Martín-Mateos,
J.A. Alonso,
M. Pérez-Jiménez,
F. Sancho-Caparrini
Molecular Computation Models in ACL2: a Simulation of Lipton's Experiment Solving SAT
[PDF] [PS] [Supporting materials]
16:30 F.J. Martín-Mateos,
J.A. Alonso,
M.J. Hidalgo,
J.L. Ruiz-Reina
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory
[PDF] [PS] [Supporting materials]
17:00   Short break
17:30 S. Ray,
R. Sumners
Verification of an In-place Quicksort in ACL2
[PDF] [PS] [Supporting materials] (Slides: [PS] [PDF])
17:50   Discussion


BORRIONE Dominique (UJF / Laboratoire TIMA)
BOUTE Raymond (Ghent University / INTEC)
CALDWELL James (University of Wyoming / Computer Science)
COWLES John (University of Wyoming / Computer Science)
GAMBOA Ruben (University of Wyoming / Computer Science)
GASCARD Eric (TIMA / Laboratoire TIMA)
GEORGELIN Philippe (UJF / Laboratoire TIMA)
GOERIGK Wolfgang (University of Kiel / Institut f. Informatik)
HUNT Warren (IBM)
JOHNSON Steven (Indiana University / Computer Science)
KAUFMANN Matt (Advanced Micro Devices, Inc.)
MANOLIOS Panagiotis (Georgia Institute of Technology / College of Computing)
MARTIN-MATEOS Francisco-Jesus (Universidad de Sevilla / CCIA)
MATLIN Olga (Argonne National Laboratory / Mathematics and Computer Science)
MEDINA-BULO Inmaculada (University of Cadiz / Lenguajes y Sistemas Informáticos)
MIDDLETON Brittany (University of Texas at Austin / Computer Science)
MOORE J Strother (University of Texas at Austin / Depart. Computer Sciences)
PALOMO-LOZANO Francisco (University of Cádiz / Lenguajes y Sistemas Informáticos)
PNUELI Amir (Weizmann Institute of Science / Computer Science)
RAY Sandip (UT Austin / CS)
RUIZ-REINA Jose-Luis (Universidad de Sevilla / CCIA)
SAWADA Jun (IBM / Research)
SENELLART Pierre (École normale supérieure (Paris) / Computer Science)
SUMNERS Robert (The University of Texas At Austin / Electrical Engineering)