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)
Contributed Talks
10:30-11:00 Iteration in ACL2. Matt Kaufmann and J Moore. (PDF, slides)
11:00-11:30 New Rewriter Features in FGL. Sol Swords. (PDF, slides)
11:30-12:00 Computing and Proving Well-founded Orderings through Finite Abstractions. Rob Sumners. (PDF, slides)
Invited Talk
2:00-3:00 Invited Talk: Adventures in Verifying Arithmetic. John Harrison. (slides)
Contributed Talks
3:30-4:00 RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2. Mertcan Temel. (PDF, slides)
4:00-4:30 Quadratic Extensions in ACL2. Ruben Gamboa, John Cowles and Woodrow Gamboa. (PDF, slides)
4:30-4:45 Type Inference Using Meta-extract for Smtlink and Beyond. Yan Peng and Mark Greenstreet. (PDF, slides)
4:45-5:00 Cauchy-Schwarz for ACL2 Abstract Vector Spaces. Carl Kwan, Yan Peng and Mark R. Greenstreet. (PDF)
5:00-5:15 Minimal fractional representations of integers mod M. David Greve. (PDF, slides)
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.
9:30-10:00 What's New in the ACL2 Community Books? Alessandro Coglio.
Contributed Talks
10:30-11:00 Generating Mutually Inductive Theorems from Concise Descriptions. Sol Swords. (PDF)
11:00-11:30 Ethereum's Recursive Length Prefix in ACL2. Alessandro Coglio.(PDF)
11:30-12:00 Isomorphic Data Type Transformations. Alessandro Coglio and Stephen Westfold. (PDF)
12:00-12:15 Put Me on the RAC. David Hardin. (PDF)
Invited Talk
2:00-3:00 Invited Talk. Leonardo de Moura.
Closing Session
3:00-4:00 Rump Session
4:00-5:00 Social Hour and Business Meeting