All times are US/Austin (GMT-5)
Thursday, May 28, 2020
Invited Talk
| 8:50-9:00 |
Welcome! Grant Passmore and Ruben Gamboa. |
| 9:00-10:00 |
Invited Talk: Formal Verification of Arithmetic RTL. David Russinoff. (PDF, slides,
video) |
Contributed Talks
| 10:30-11:00 |
Iteration in ACL2. Matt Kaufmann and J Moore. (PDF, slides,
video)
|
| 11:00-11:30 |
New Rewriter Features in FGL. Sol Swords. (PDF, slides,
video) |
| 11:30-12:00 |
Computing and Proving Well-founded Orderings through Finite Abstractions. Rob Sumners. (PDF, slides,
video) |
Invited Talk
| 2:00-3:00 |
Invited Talk: Adventures in Verifying Arithmetic. John Harrison. (slides,
video) |
Contributed Talks
| 3:30-4:00 |
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2. Mertcan Temel. (PDF, slides,
video) |
| 4:00-4:30 |
Quadratic Extensions in ACL2. Ruben Gamboa, John Cowles and Woodrow Gamboa. (PDF, slides,
video) |
| 4:30-4:45 |
Type Inference Using Meta-extract for Smtlink and Beyond. Yan Peng and Mark Greenstreet. (PDF, slides,
video) |
| 4:45-5:00 |
Cauchy-Schwarz for ACL2 Abstract Vector Spaces. Carl Kwan, Yan Peng and Mark R. Greenstreet. (PDF, slides,
video)
|
| 5:00-5:15 |
Minimal fractional representations of integers mod M. David Greve. (PDF, slides,
video) |
Social Time
| 6:30- |
Virtual Happy Hour |
Friday, May 29, 2020
The News Hour
| 9:00-9:30 |
What's New in ACL2? Matt Kaufmann and J Moore.
(slides,
video) |
| 9:30-10:00 |
What's New in the ACL2 Community Books? Alessandro Coglio.
(slides,
video) |
Contributed Talks
| 10:30-11:00 |
Generating Mutually Inductive Theorems from Concise Descriptions. Sol Swords. (PDF, slides,
video) |
| 11:00-11:30 |
Ethereum's Recursive Length Prefix in ACL2. Alessandro Coglio.(PDF, slides,
video) |
| 11:30-12:00 |
Isomorphic Data Type Transformations. Alessandro Coglio and Stephen Westfold. (PDF, slides,
video) |
| 12:00-12:15 |
Put Me on the RAC. David Hardin.
(PDF,
video) |
Invited Talk
| 2:00-3:00 |
Invited Talk: Lean in Lean. Leonardo de Moura. (slides,
video) |
Closing Session
| 3:00-4:00 |
Rump Session |
| 3:00-3:15 |
Rump Talk: Jenkins CI. David Rager. |
| 3:15-3:30 |
Rump Talk: New Features in Java Code Generator. Alessandro Coglio. (slides,
video) |
| 3:30-3:45 |
Rump Talk: Avoiding Useless Rules. Matt Kaufmann. (slides,
video) |
| 3:45-4:00(ish) |
Rump Talk: Loop$ Recursion and Current Work. J Moore. (session log,
video) |
| 4:00(ish)-5:00 |
Social Hour and Business Meeting |