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


Sunday, November 4: Welcome Reception
18:00 -
(may end a bit later)
Welcome Reception -- dinner will be served (buffet style)
House of Holly Bell and Matt Kaufmann
2203 Euclid Ave., Austin, TX
Usually there's plenty of nearby parking on the street; or you can take a bus from the UT campus (also see the bus website).
Significant others are welcome!
Monday, November 5: Day 1
  Session 1 (chair: Matt Kaufmann)
09:00 Welcome
09:10 Sandip Ray
(University of Florida at Gainesville)
Invited talk 1
Small Team, Short Ramp, Industrial-scale Problems: Some Experiments in the Practicum of Interactive Theorem Proving
10:10 Sol Swords Incremental SAT Library Integration using Abstract Stobjs
10:40 BREAK
  Session 2 (chair: Warren Hunt)
11:00 Mihir Mehta Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
11:30 Alessandro Coglio
Shilpi Goel
Adding 32-bit Mode to the ACL2 Model of the x86 ISA
[Keynote slides, with animations]
[PDF slides, with simpler animations]
[PDF slides, with no animations]
12:00 Alessandro Coglio A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
[Animated PowerPoint Show file (viewable with free PowerPoint Viewer)]
[PDF slides (not animated)]
12:30 LUNCH
  Session 3 (chair: Shilpi Goel)
14:00 Sol Swords
(Centaur Technology)
Invited talk 2
Building Blocks for RTL Verification in ACL2
15:00 David Hardin
Konrad Slind
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems
15:30 BREAK
  Session 4 (chair: Anna Slobodova)
15:50 Rob Sumners A Toolbox for Property Checking from Simulation Using Incremental SAT (Extended Abstract)
16:10 Rump Session talks
16:40 BREAK
  Session 5 (chair: Alessandro Coglio)
17:00 David Greve
Andrew Gacek
Trapezoidal Generalization over Linear Constraints
17:30 Rump Session talks
18:00 Day 1 program ends
18:30 -
CONFERENCE DINNER Aster's Ethiopian Restaurant
2804 N Interstate 35 Austin, TX 78705
[Map from workshop]
6:30 to 9:00 (wine at 6:30; buffet at 7:00)
[For those who want to hang out afterwards, one possibility is to Bennu Coffee.]
Tuesday, November 6: Day 2
  Session 1 (chair: David Russinoff)
09:00 Alastair Reid
Invited talk 3
Creating Formal Specifications of the Arm Processor Architecture
10:00 Ruben Gamboa
John Cowles
The Fundamental Theorem of Algebra in ACL2
10:30 Rump Session talk
10:40 BREAK
  Session 2 (chair: Ruben Gamboa)
11:00 Carl Kwan
Mark Greenstreet
Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r)
[Slides] (includes next talk)
11:30 Carl Kwan
Mark Greenstreet
Convex Functions in ACL2(r)
[Slides] (includes preceding talk)
12:00 Yan Peng
Mark Greenstreet
Smtlink 2.0
12:30 LUNCH
  Session 3 (chair: David Rager)
14:00 Alessandro Coglio What's New in the Community Books
14:30 Matt Kaufmann DefunT: A Tool for Automating Termination Proofs by Using the Community Books (Extended Abstract)
[Slides [Without pauses] [With pauses]]
14:50 Matt Kaufmann
J Moore
What's New in the ACL2 System
[Slides (not including :doc topics)]
[Video (you may want to skip to the 2:29 mark; the fun starts within 15 seconds from there)]
15:20 BREAK
  Session 4 (chair: Dave Greve)
15:40 Sol Swords Hint Orchestration Using ACL2's Simplifier
16:10 Rump Session talks
16:40 BREAK
  Session 5
17:00 Business Meeting Tentative list of topics is here.
18:00 Workshop ends