| Sunday, May 21: Welcome Reception | ||
| 18:00 - 21:00 |
Welcome Reception -- food will be served House of Anna Slobodova and Warren Hunt 2106 Ringtail Ridge, Austin, TX [Directions from Austin Folk House] [Directions from The Quarters at Hardin House] ] |
|
| Monday, May 22: Day 1 | ||
| 08:30 | COFFEE and SNACKS | |
| 09:00 | Welcome | |
| Session 1 | ||
| 09:10 | Grant Passmore (Aesthetic Integration) |
Invited talk 2 Formal Verification of Financial Algorithms, Progress and Prospects |
| 10:10 | Shilpi Goel | The x86isa Books: Features, Usage, and Future Plans |
| 10:40 | BREAK | |
| Session 2 | ||
| 11:00 | John Cowles Ruben Gamboa |
The Cayley-Dickson Construction in ACL2 |
| 11:30 | David Russinoff | A Computationally Surveyable Proof of the Group Properties of an Elliptic Curve |
| 12:00 | LUNCH | |
| Session 3 | ||
| 13:30 | Rump Session 1 (20 minute talks) |
|
| 15:15 | BREAK | |
| Session 4 | ||
| 15:30 | Matt Kaufmann Sol Swords |
Meta-extract: Using Existing Facts in Meta-reasoning |
| 16:00 | Alessandro Coglio Matt Kaufmann Eric W. Smith |
A Versatile, Sound Tool for Simplifying Definitions |
| 16:30 | Rump Session 2 (20 minute talks) |
|
| 17:30 (tentative) |
End of first day's program | |
| 18:30 - 21:30 |
CONFERENCE DINNER | Manuel's
downtown 310 Congress Avenue, Austin, Texas 78701 (map) |
| Tuesday, May 23: Day 2 | ||
| 08:30 | COFFEE and SNACKS | |
| Session 5 | ||
| 09:00 | Glenn Henry (Centaur Technology) |
Invited talk 1 Using Mechanized Mathematics in an Organization with a Simulation-Based Mentality |
| 10:00 | Rob Sumners | Proof Reduction of Fair Stuttering Refinement of Asynchronous Systems and Applications |
| 10:30 | BREAK | |
| Session 6 | ||
| 11:00 | Sol Swords | Term-Level Reasoning in Support Of Bit-Blasting |
| 11:30 | Cuong Chau | Extended Abstract: Formal Specification and Verification of the FM9001 Microprocessor Using the DE System |
| 11:50 | Rump Session 3 (20 minute talks) |
|
| 12:10 | LUNCH | |
| Session 7 | ||
| 13:30 | Greg Grohoski (Oracle) |
Invited talk 3 Verifying Oracle's SPARC Processors with ACL2 |
| 14:00 | Matt Kaufmann | What's new in the ACL2 system |
| 14:30 | Alessandro Coglio Sol Swords (and others?) |
What's new in the community books |
| 15:00 | BREAK | |
| Session 8 | ||
| 15:30 | Business Meeting and Discussion |
|
| 16:30 | Rump Session 4 (15 minute talks) |
|
| 17:30 (tentative) | Workshop ends | |