Notes:
| Sunday, November 12: Day 0 | ||
| 19:30 - 21:30 |
RECEPTION | Outdoors at: Meanwhile Brewing 3901 Promontory Point Dr, Austin, TX 78744 https://www.meanwhilebeer.com/ |
| Monday, November 13: Day 1 | ||
| 08:30 | COFFEE and SNACKS | |
| Session 1 (chair: Alessandro Coglio) | ||
| 09:00 | Welcome | |
| 09:10 | Eric Smith (Kestrel Institute) |
Invited talk 1 Formal Verification with Axe and ACL2 |
| 10:10 | Grant Passmore | ACL2 Proofs of Nonlinear Inequalities with Imandra |
| 10:40 | BREAK | |
| Session 2 (chair: Mark Greenstreet) | ||
| 11:10 | David Russinoff | A Formalization of Finite Group Theory: Part II |
| 11:40 | David Russinoff | A Formalization of Finite Group Theory:
Part III (For slides, see link above for Part II.) |
| 12:10 | LUNCH BREAK (lunch not provided) | |
| Session 3 (chair: Mertcan Temel) | ||
| 13:40 | Alessandro Coglio (speaker) Eric McCarthy Eric Smith |
Formal Verification of Zero-Knowledge Circuits [Note: The link above is to a pdf; here is a link to the animated (.ppsx) version] |
| 14:10 | Ruben Gamboa (speaker) Panagiotis Manolios Eric Smith Kyle Thompson |
Using Counter-Example Generation and Theory Exploration to Suggest Missing Hypotheses |
| 14:40 | BREAK | |
| Session 4 (chair: Eric McCarthy) | ||
| 15:00 | Carl Kwan Yutong Xin (speaker) William D. Young |
CHERI Concentrate in ACL2 [extended abstract] |
| 15:20 | Carl Kwan | Classical LU Decomposition in ACL2 [extended abstract] |
| 15:40 | David Hardin | Verification of a Rust Implementation of Knuth's Dancing Links using ACL2 |
| 16:10 | BREAK | |
| Session 5 (chair: Sol Swords) | ||
| 16:30 | Rump Session 1 |
|
| 17:00 | Business Meeting and Technical Discussion | |
| 18:00 | Day 1 program ends | |
| 19:00 - 21:30 |
CONFERENCE DINNER (BANQUET) | Fresa's South First 1703 S. 1st St., Austin, TX 78704 https://www.fresaschicken.com/ |
| Tuesday, November 14: Day 2 | ||
| 08:30 | COFFEE and SNACKS | |
| Session 1 (chair: Shilpi Goel) | ||
| 09:00 | Jim Grundy (Amazon Web Services) |
Invited talk 2 Applying Formal Verification to Make a Difference |
| 10:00 | Max von Hippel (speaker) Panagiotis Manolios Ken McMillan Cristina Nita-Rotaru Lenore Zuck |
A Case Study in Analytic Protocol Analysis in ACL2 |
| 10:30 | BREAK | |
| Session 2 (chair: Warren Hunt) | ||
| 11:00 | Ankit Kumar (speaker) Max von Hippel Panagiotis Manolios Cristina Nita-Rotaru |
Verification of GossipSub in ACL2s |
| 11:30 | Andrew T. Walter (speaker) Ankit Kumar Panagiotis Manolios |
Proving Calculational Proofs Correct |
| 12:00 | LUNCH BREAK (lunch not provided) | |
| Session 3 (chair: Anna Slobodova) | ||
| 13:30 | Matt Kaufmann (speaker) J Moore |
What's New in the ACL2 System |
| 14:30 | Rump Session 2 |
|
| 14:45 | BREAK | |
| Session 4 (chair: J Moore) | ||
| 15:05 | Alessandro Coglio | What's New in the Community Books |
| 16:05 | Sol Swords | A Bound-Finding Tool for Arithmetic Terms [extended abstract] |
| 16:25 | BREAK | |
| Session 5 (chair: Rob Sumners) | ||
| 16:35 | Matt Kaufmann J Moore |
Advances in ACL2 Proof Debugging Tools |
| 17:05 | Rump Session 3 |
|
| 17:50 | Workshop ends | |
NOTE: If you'd like to join in an informal post-workshop dinner, let Matt Kaufmann know before 10 am Tuesday, Nov. 14. Details are here.