ACL2 Workshop 2020 Program

ACL2 Workshop 2020 Program

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