13th International Workshop on the
ACL2 Theorem Prover and Its Applications


Thursday, October 1: Day 1
08:30 Snack and greet Not a full breakfast (so most will want to eat at their hotel), but there will be a few pastries or muffins
09:00 Welcome
  Session 1 (Chair: Matt Kaufmann)
09:10 J Strother Moore Invited keynote talk
Lessons Learned over 45 Years in Theorem Proving
10:10 David L. Rager
Jo Ebergen
Austin Lee
Dmitry Nadezhin
Ben Selfridge
Cuong Kim Chau
(Extended Abstract)
A Brief Introduction to Oracle's Use of ACL2 in Verifying Floating-point and Integer Arithmetic
10:30 Break
  Session 2 (Chair: Dave Greve)
11:00 Sol Swords
Jared Davis
Fix Your Types
11:30 Alessandro Coglio Second-Order Functions and Theorems in ACL2
[Slides (PDF) (Powerpoint: The animated version is viewable with PowerPoint, or with the free PowerPoint Viewer from Microsoft, which seems to exist only for Windows.)]
12:00 Rump Session 1 12:00 - 12:20: Eric Smith, Software Synthesis with ACL2
[Slides (PDF) (Powerpoint)]
12:30 Lunch (near the workshop room)
  Session 3 (Chair: Warren A. Hunt, Jr.)
Industrial Use of ACL2: Present and Future

Jo Ebergen, Oracle
David Hardin, Rockwell Collins
David Russinoff, Intel
Rob Sumners, AMD
Sol Swords, Centaur
14:30 Break
  Session 4 (Chair: Anna Slobodova)
15:00 Cuong K. Chau
Matt Kaufmann
Warren A. Hunt, Jr.
Fourier Series Formalization in ACL2(r)
15:30 John Cowles
Ruben Gamboa
Perfect Numbers in ACL2
16:00 Rump Session 2 16:00 - 16:20: Matt Kaufmann, A challenge problem: Toward better ACL2 proof technique
[Slides without pauses] [Slides with pauses]
16:20 Break
  Session 5 (Chair: Jared Davis)
16:45 Rump Session 3 16:45 - 17:05: David Russinoff, 2^255 - 19 is Prime: Toward Verified Elliptic Curve Cryptography
17:05 - 17:25: Eric Smith, Verifying Android apps with ACL2
[Slides (PDF) (Powerpoint)]
17:25 - 17:45: J Moore, Adding LOOP to ACL2
[Log of demo]
18:00 End of first day's program
18:30 to 21:30 Banquet
Trudy's Texas Star, 409 West 30th Street, Austin, Texas
Maps: path from workshop and path from Austin Folk House B&B
Friday, October 2: Day 2
08:30 Snack and greet Not a full breakfast (so most will want to eat at their hotel), but there will be a few pastries or muffins
  Session 6 (Chair: David L. Rager)
09:00 John O'Leary Invited keynote talk
Verification in the Age of Integration
10:00 Yan Peng
Mark Greenstreet
Extending ACL2 with SMT Solvers
10:30 Break
  Session 7 (Chair: Eric Smith)
11:00 David S. Hardin Reasoning about LLVM code using Codewalker
11:30 J Strother Moore Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
[Slides] [Demo]
12:00 Mitesh Jain
Panagiotis Manolios
Proving Skipping Refinement with ACL2s
12:30 Lunch (near the workshop room)
  Session 8 (Chair: David Hardin)
13:30 Rump Session 4 13:30 - 13:45: Dave Greve, def::ung Enhancements
13:45 - 14:00: David Rager, Maintaining community [in]sanity with Jenkins and Github
Relevant links:
14:00 Jared Davis What's New in the Community Books
14:30 Matt Kaufmann
J Strother Moore
What's New in the ACL2 system
15:00 Break
  Session 9 (Chairs: Matt Kaufmann and David L. Rager)
15:30 Additional rump session talks:
Shilpi Goel will talk on the x86isa books for 15 minutes;
Warren Hunt will talk on CCL compiler work for 10 minutes.

Business Meeting and Discussion (see page of possible topics)
17:00 Workshop ends