| 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 | |