Day 1 Schedule, ACL2-2004

For full workshop information, please visit the workshop's home page,

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