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

GENERAL INFORMATION
PRESENTATIONS
PARTICIPANTS
PROGRAM COMMITTEE
ORGANIZING COMMITTEE
Affiliated with
ETAPS 2002



GENERAL INFORMATION

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 http://www.cs.utexas.edu/users/moore/acl2.

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.




PRESENTATIONS

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



PARTICIPANTS

AUSTEL Vernon (IBM) austel@us.ibm.com
BORRIONE Dominique (UJF / Laboratoire TIMA) dominique.borrione@imag.fr
BOUTE Raymond (Ghent University / INTEC) boute@intec.rug.ac.be
CALDWELL James (University of Wyoming / Computer Science) jlc@cs.uwyo.edu
COWLES John (University of Wyoming / Computer Science) cowles@uwyo.edu
GAMBOA Ruben (University of Wyoming / Computer Science) ruben@cs.uwyo.edu
GASCARD Eric (TIMA / Laboratoire TIMA) eric.gascard@imag.fr
GEORGELIN Philippe (UJF / Laboratoire TIMA) philippe.georgelin@imag.fr
GOERIGK Wolfgang (University of Kiel / Institut f. Informatik) wg@informatik.uni-kiel.de
HUNT Warren (IBM) whunt@austin.ibm.com
JOHNSON Steven (Indiana University / Computer Science) sjohnson@cs.indiana.edu
KAUFMANN Matt (Advanced Micro Devices, Inc.) matt.kaufmann@amd.com
MANOLIOS Panagiotis (Georgia Institute of Technology / College of Computing) manolios@cc.gatech.edu
MARTIN-MATEOS Francisco-Jesus (Universidad de Sevilla / CCIA) francisco-jesus.martin@cs.us.es
MATLIN Olga (Argonne National Laboratory / Mathematics and Computer Science) matlin@mcs.anl.gov
MEDINA-BULO Inmaculada (University of Cadiz / Lenguajes y Sistemas Informáticos) inmaculada.medina@uca.es
MIDDLETON Brittany (University of Texas at Austin / Computer Science) brittany@cs.utexas.edu
MOORE J Strother (University of Texas at Austin / Depart. Computer Sciences) moore@cs.utexas.edu
PALOMO-LOZANO Francisco (University of Cádiz / Lenguajes y Sistemas Informáticos) francisco.palomo@uca.es
PNUELI Amir (Weizmann Institute of Science / Computer Science) amir@wisdom.weizmann.ac.il
RAY Sandip (UT Austin / CS) sandip@cs.utexas.edu
RUIZ-REINA Jose-Luis (Universidad de Sevilla / CCIA) jose-luis.ruiz@cs.us.es
SAWADA Jun (IBM / Research) sawada@us.ibm.com
SENELLART Pierre (École normale supérieure (Paris) / Computer Science) pierre@senellart.com
SUMNERS Robert (The University of Texas At Austin / Electrical Engineering) robert.sumners@amd.com




PROGRAM COMMITTEE




ORGANIZING COMMITTEE