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

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
11:55 J. L. Caldwell,
J. R. Cowles
How to Believe a Nuprl Proof: checking Nuprl Proofs in ACL2
12:15 J. Sawada Formal Verification of Divide and Square Root Algorithms Using Series Calculation
12:45   Lunch
14:15 R. A. Gamboa,
B. E. Middleton
Taylor's Formula with Remainder
14:45 I. Medina-Bulo,
F. Palomo-Lozano,
J. A. Alonso-Jiménez
Implementation in ACL2 of Well-Founded Polynomial Orderings
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
15:55 J.-L. Ruiz-Reina,
J.-A. Alonso,
M.-J. Hidalgo,
F.J. Martín-Mateos
Progress Report: Term Dags Using Stobjs
16:15   Coffee break
16:45 P. Manolios,
M. Kaufmann
Adding a Total Order to ACL2
17:15 M. Kaufmann,
J Moore
What's New in ACL2?
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
11:15 R. Sumners,
M. Kaufmann
Efficient Rewriting of Data Structures in ACL2
11:35   Short break
11:55 J. Cowles Flat Domains and Recursive Equations in ACL2
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
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
17:00   Short break
17:30 Sandip Ray,
Rob Sumners
Verification of an In-place Quicksort in ACL2
17:55   Discussion