| Thursday, October 1: Day 1 | ||
| 08:30 | Snack and greet | Not a full breakfast (so most will want to eat at their hotel), but there will be a few pastries or muffins |
| 09:00 | Welcome | |
| Session 1 (Chair: Matt Kaufmann) | ||
| 09:10 | J Strother Moore | Invited keynote
talk Lessons Learned over 45 Years in Theorem Proving |
| 10:10 | David L. Rager Jo Ebergen Austin Lee Dmitry Nadezhin Ben Selfridge Cuong Kim Chau |
(Extended Abstract) A Brief Introduction to Oracle's Use of ACL2 in Verifying Floating-point and Integer Arithmetic [Slides] |
| 10:30 | Break | |
| Session 2 (Chair: Dave Greve) | ||
| 11:00 | Sol Swords Jared Davis |
Fix Your Types [Slides] |
| 11:30 | Alessandro Coglio | Second-Order Functions and Theorems in ACL2 [Slides (PDF) (Powerpoint: The animated version is viewable with PowerPoint, or with the free PowerPoint Viewer from Microsoft, which seems to exist only for Windows.)] |
| 12:00 | Rump Session 1 | 12:00 - 12:20: Eric
Smith, Software
Synthesis with ACL2 [Slides (PDF) (Powerpoint)] |
| 12:30 | Lunch (near the workshop room) | |
| Session 3 (Chair: Warren A. Hunt, Jr.) | ||
| 13:30 | PANEL | PANEL Industrial Use of ACL2: Present and Future Jo Ebergen, Oracle David Hardin, Rockwell Collins David Russinoff, Intel Rob Sumners, AMD Sol Swords, Centaur |
| 14:30 | Break | |
| Session 4 (Chair: Anna Slobodova) | ||
| 15:00 | Cuong K. Chau Matt Kaufmann Warren A. Hunt, Jr. |
Fourier Series
Formalization in ACL2(r) [Slides] |
| 15:30 | John Cowles Ruben Gamboa |
Perfect Numbers in ACL2 [Slides] |
| 16:00 | Rump Session 2 | 16:00 - 16:20: Matt
Kaufmann, A
challenge problem: Toward better ACL2 proof
technique [Slides without pauses] [Slides with pauses] |
| 16:20 | Break | |
| Session 5 (Chair: Jared Davis) | ||
| 16:45 | Rump Session 3 | 16:45 - 17:05: David Russinoff, 2^255 - 19 is Prime: Toward Verified Elliptic Curve Cryptography 17:05 - 17:25: Eric Smith, Verifying Android apps with ACL2 [Slides (PDF) (Powerpoint)] 17:25 - 17:45: J Moore, Adding LOOP to ACL2 [Log of demo] |
| 18:00 | End of first day's program | |
| 18:30 to 21:30 | Banquet Trudy's Texas Star, 409 West 30th Street, Austin, Texas Maps: path from workshop and path from Austin Folk House B&B |
|
| Friday, October 2: Day 2 | ||
| 08:30 | Snack and greet | Not a full breakfast (so most will want to eat at their hotel), but there will be a few pastries or muffins |
| Session 6 (Chair: David L. Rager) | ||
| 09:00 | John O'Leary | Invited keynote talk Verification in the Age of Integration |
| 10:00 | Yan Peng Mark Greenstreet |
Extending ACL2 with SMT Solvers [Slides] |
| 10:30 | Break | |
| Session 7 (Chair: Eric Smith) | ||
| 11:00 | David S. Hardin | Reasoning about LLVM code using Codewalker [Slides] |
| 11:30 | J Strother Moore | Stateman: Using Metafunctions to Manage Large Terms
Representing Machine
States [Slides] [Demo] |
| 12:00 | Mitesh Jain Panagiotis Manolios |
Proving Skipping Refinement with ACL2s [Slides] |
| 12:30 | Lunch (near the workshop room) | |
| Session 8 (Chair: David Hardin) | ||
| 13:30 | Rump Session 4 |
13:30 - 13:45: Dave Greve, def::ung Enhancements [Slides] 13:45 - 14:00: David Rager, Maintaining community [in]sanity with Jenkins and Github Relevant links: http://leeroy.defthm.com:DOC
GIT-QUICK-START
|
| 14:00 | Jared Davis | What's New in the Community Books |
| 14:30 | Matt Kaufmann J Strother Moore |
What's New in the ACL2 system |
| 15:00 | Break | |
| Session 9 (Chairs: Matt Kaufmann and David L. Rager) | ||
| 15:30 |
Additional rump session talks: Shilpi Goel will talk on the x86isa books for 15 minutes; Warren Hunt will talk on CCL compiler work for 10 minutes. Business Meeting and Discussion (see page of possible topics) |
|
| 17:00 | Workshop ends | |