NOTES:
| Sunday, May 11: Day 0 | |||
| 19:30 – 21:30 |
RECEPTION | Love Supreme Pizza Bar 2805 Manor Rd. Austin, TX 78722 https://www.lovesupremepizzabar.com |
|
| Monday, May 12: Day 1 | |||
| 08:30 | COFFEE and SNACKS | ||
| Session 1 (chair: Pete Manolios) | |||
| 09:00 | Welcome from Matt Kaufmann and Eric Smith | ||
| 09:10 | Swarat Chaudhuri (UT Austin) | Invited talk 1 Scaling Formal Verification with Machine Learning |
|
| 10:10 | BREAK | ||
| Session 2 (chair: TBD) | |||
| 10:30 | David Russinoff | A Formalization of Elementary Linear Algebra: Part I | |
| 11:00 | David Russinoff | A Formalization of Elementary Linear Algebra: Part II | |
| 11:30 | LUNCH BREAK (lunch not provided) | ||
| Session 3 (chair: TBD) | |||
| 13:00 | Grant Jurgensen | A Proof of the Schröder-Bernstein Theorem in ACL2 |
|
| 13:30 | Matt Kaufmann (speaker) J Strother Moore |
What's New with the ACL2 System? | |
| 14:00 | Zeke Medley (speaker) Panagiotis Manolios |
Cellular Automata Surviving k Steps | |
| 14:30 | BREAK | ||
| Session 4 (chair: TBD) | |||
| 15:00 | Carl Kwan | [Extended Abstract] RV32I in ACL2 | |
| 15:20 | Mayank Manjrekar | [Extended Abstract] On Automating Proofs of Multiplier Adder Trees using the RTL Books | |
| 15:40 | Matt Kaufmann (speaker) Warren A. Hunt, Jr. Yahya Sohail |
[Extended Abstract] Mutable Objects with Several Implementations | |
| 16:00 | Matt Kaufmann (speaker) J Strother Moore | [Extended Abstract] Partial-encapsulate and Its Support for Floating-point Operations in ACL2 | |
| 16:20 | BREAK | ||
| Session 5 (chair: TBD) | |||
| 16:45 | Rump Session 1 (See the abstracts page for talks accepted so far.) |
|
|
| 18:00 | Day 1 program ends | ||
| 19:00 – 21:30 |
CONFERENCE DINNER (BANQUET) | Machi Sushi 2200 S I-35 Frontage Rd. Austin, TX 78704 https://machisushiaustin.com |
|
| Tuesday, May 13: Day 2 | |||
| 08:30 | COFFEE and SNACKS | ||
| Session 6 (chair: Ruben Gamboa) | |||
| 09:00 | Warren A. Hunt, Jr. (UT Austin) Anna Slobodova (Arm Ltd) |
Invited talk 2 The Future of ACL2 Community |
|
| 10:00 | BREAK | ||
| Session 7 (chair: TBD) | |||
| 10:30 | Alessandro Coglio (speaker) Eric McCarthy |
A Formalization of the Yul Language and Some Verified Yul Code Transformations | |
| 11:00 | Alessandro Coglio | What's New with the ACL2 Books? | |
| 11:30 | LUNCH BREAK (lunch not provided) | ||
| Session 8 (chair: TBD) | |||
| 13:00 | Ankit Kumar (speaker) Panagiotis Manolios |
A Formalization of the Correctness of the Floodsub Protocol | |
| 13:30 | Andrew T. Walter (speaker) Panagiotis Manolios |
An ACL2s Interface to Z3 | |
| 14:00 | Samuel Xifaras (speaker) Panagiotis Manolios Andrew T. Walter William Robertson |
An Enumerative Embedding of the Python Type System into ACL2s | |
| 14:30 | BREAK | ||
| Session 9 (chair: TBD) | |||
| 15:00 | Rump Session 2 (See the abstracts page for talks accepted so far.) |
|
|
| 16:00 | BREAK | ||
| Session 10 (chair: Pete Manolios) | |||
| 16:30 | Business Meeting (possible agenda) | ||
| 18:00 | Workshop ends | ||