For full workshop information, please visit the workshop's home page, http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/.
| 8:30 | Breakfast | |
| 9:00 | Welcome | |
| Session 1 (Chair: Matt Kaufmann) | ||
| 9:05 | Rob Sumners (speaker), Sandip Ray |
Reducing Invariant Proofs to Finite Search via Rewriting |
| 9:35 | Sandip Ray | Attaching Efficient Executability to Partial Functions in ACL2 |
| 9:55 | John Matthews (speaker), Daron Vroon |
Partial Clock Functions in ACL2 |
| 10:25 | Long break | |
| Session 2 (Chair: Vernon Austel) | ||
| 10:55 | Marcio Gameiro (speaker), Panagiotis Manolios |
Formally Verifying an Algorithm Based on Interval Arithmetic for Checking Transversality |
| 11:25 | Panagiotis Manolios, Sudarshan K. Srinivasan (speaker) |
A Suite of Hard ACL2 Theorems Arising in Refinement-Based Processor Verification |
| 11:45 | Jared Davis | Finite Set Theory based on Fully Ordered Lists |
| 12:15 | Lunch | |
| Session 3 (Chair: Jose Luis Ruiz-Reina) | ||
| 14:00 | Steve Roach, Fares Fraij (speaker) |
Verifying Transformation Rules of the HATS High-Assurance Transformation System: An Approach |
| 14:20 | Kathi Fisler (speaker), Brian Roberts |
A Case Study in using ACL2 for Feature-Oriented Verification |
| 14:40 | Matt Kaufmann, J Moore, ALL |
ACL2 Directions |
| 15:10 | Long break | |
| Session 4 (Chair: Warren Hunt) | ||
| 15:40 | Jun Sawada | ACL2VHDL Translator: A Simple Approach to Fill the Semantic Gap |
| 16:10 | Vernon Austel | Adding a typing mechanism to ACL2 |
| 16:30 | Short break | |
| Session 5 (Chair: Pete Manolios) | ||
| 16:50 | J.L. Ruiz Reina (speaker), J.A. Alonso, M.J. Hidalgo, F.J. Martin-Mateos |
A Formally Verified Quadratic Unification Algorithm |
| 17:20 | ALL | General Discussion (e.g., ACL2 enhancements) |
| 18:00 | End of first day | |