Note: The copyrights for all the papers posted here belong to the ACL2 Steering Committee.

Day 1 (Monday, May 11)
8:50-9:00 Sandip Ray and
David Russinoff
Welcome and Opening Remarks
Session 1
Chair: Matt Kaufmann
9:00-9:25 Rob Sumners User Control and Direction of a More Efficient Simplifier in ACL2
[paper] [slides] [supporting materials]
9:25-9:50 J Moore Automatically Computing Functional Instantiations
[paper] [slides] [supporting materials]
9:50-10:05 Robert S. Boyer and
Warren A. Hunt, Jr.
Symbolic Simulation in ACL2
[paper]
10:05-10:20 Hanbing Liu Proving A Specific Type Of Inequality Theorems in ACL2:
a bind-free experience report
[paper] [slides] [supporting materials]
10:20-10:35 Short Break
Session 2
Chair: Ruben Gamboa
10:35-10:50 Rex Page Computational Logic in the Undergraduate Curriculum
[paper]
10:50-11:15 Carl Eastlund and
Matthias Felleisen
Automatic Verification of Interactive Graphical Programs
[paper]
11:15-11:30 Carl Eastlund DoubleCheck Your Theorems
[paper]
11:30-11:55 Antonio Garcia-Dominguez,
Francisco Palomo-Lozano, and
Inmaculada Medina-Bulo
Hypertext Navigation of ACL2 Proofs with XMLEye
[paper] [slides]
11:55-13:25 Lunch Break
Session 3
Chair: Rex Page
13:25-13:50 Ruben Gamboa and
John Cowles
Inverse Functions in ACL2(r)
[paper] [slides] [supporting materials]
13:50-14:15 Matt Kaufmann Abbreviated Output for Input in ACL2
[paper] [slides]
14:15-15:00 Matt Kaufmann and
J Moore
New and Desired Features of ACL2
[presentation]
15:00-15:30 Long Break
Session 4
Chair: Francisco Palomo-Lozano
15:30-15:45 Ryan Ralston ACL2-Certified AVL Trees
[paper] [slides]
15:45-16:00 Fares Fraij and
Steve Roach
Proof of Transitive Closure Property of Directed Acyclic Graphs
[paper] [supporting materials]
16:00-16:15 John Cowles and
Ruben Gamboa
\triangle = \square
[paper] [slides] [supporting materials]
16:15-16:30 Short Break
Session 5
Panel Session, Moderator: Panagiotis Manolios
16:30-18:00 Arvind
Matthias Felleisen
David Hardin
Wilfred Legato
Paul Miner
J Moore
What is the Future of Theorem Proving?
[Abstract] [slides: Arvind, Legato, Miner]
19:30-21:00 Workshop Dinner
Massimino's Restaurant, 207 Endicott Street [Directions]
Day 2 (Tuesday, May 12)
Session 6
Chair: Rob Sumners
9:00-9:25 Matt Kaufmann,
Jacob Kornerup, and
Mark Reitblatt
Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover
[paper] [slides] [supporting materials]
9:25-9:50 Laurence Pierre,
Renauld Clavel, and
Regis Leveugle
ACL2 for the Verification of Fault-Tolerance Properties: First Results
[paper] [slides] [supporting materials]
9:50-10:15 David Hardin and
Samuel Hardin
Efficient, Formally Verifiable Data Structures using ACL2 Single-Threaded
Objects for High-Assurance Systems
[paper] [slides] [supporting materials]
10:15-10:30 David Rager An Executable Model for Security Protocol JFKr
[paper] [supporting materials]
10:30-11:00 Long Break
Session 7 (Rump Session)
Chair: Julien Schmaltz
11:00-11:10 Ruben Gamboa and
John Cowles
The Chain Rule and Friends in ACL2(r)
[abstract] [slides]
11:10-11:15 James Caldwell,
John Cowles, and
Ruben Gamboa
Enumerating Rationals Without Repetitions
[abstract] [slides]
11:15-11:25 Harsh R. Chamarthi,
Peter C. Dillinger, and
Panagiotis Manolios
A General Data-definition Framework and Random Testing in ACL2
[abstract]
11:25-11:35 Peter C. Dillinger and
Panagiotis Manolios
ACL2 Sedan: 2009 Model Year
[abstract]
11:35-11:45 Sol Swords GL: A Verified Symbolic Execution Framework in the ACL2 Logic
[abstract] [slides]
11:45-11:55 Jared Davis ACL2-Books Repository
[abstract] [slides]
11:55-13:25 Lunch break
Session 8
Chair: J Moore
13:25-14:15 Clark Barrett
(Invited Keynote)
From SAT to SMT: Successes and Challenges
[abstract] [slides]
14:15-14:30 Short break
Session 9
Chair: John Cowles
14:30-14:45 Dave Greve Automated Reasoning With Quantified Formulae
[paper] [slides] [supporting materials]
14:45-15:10 Dave Greve Assuming Termination
[paper] [slides] [supporting materials]
15:10-15:20 Short break
Session 10
Chair: David Russinoff
15:20-15:35 Tom van den Broek and
Julien Schmaltz
A Generic Implementation Model for the Formal Verification of Networks-on-Chips
[paper] [slides] [supporting materials]
15:35-16:00 Freek Verbeek and
Julien Schmaltz
Formal Validation of Deadlock Prevention in Networks-on-Chips
[paper] [slides] [supporting materials]
16:00-16:10 Short break
Session 11 (Rump Session)
Chair: Warren Hunt
16:10-16:20 Dave Greve Untyped Types
[slides]
16:20-16:30 Carl Eastlund Modular ACL2
[abstract]
16:30-16:40 Panagiotis Manolios and
Aaron Turon
All-Termination(T)
[abstract] [slides]
16:40-16:50 Eric Smith How We Extended ACL2 to Verify Block Cipher Implementations
[abstract][slides]
16:50-17:00 Short break
Session 12
Chair: Sandip Ray
17:00-17:30 Matt Kaufmann and
J Moore
Discussion on Future Enhancements to ACL2
17:30-18:00 All Business Meeting
Workshop ends