| 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 |