ETAPS 2002
|
Affiliated with ETAPS 2002
|
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:
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 | |
| 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 |
Dominique.Borrione@imag.fr)
matt.kaufmann@amd.com)
moore@cs.utexas.edu)