The proceedings for ACL2 2006 are now available online for $9.99, at lulu.com.
|
Tuesday, August 15 Workshop, Day 1 | |||
| 8:50-9:00 |
Pete Manolios and Matt Wilding |
Welcome and Opening Remarks | Session 1, Chair: J Strother Moore |
| 9:00-9:30 | Lee Pike, Mark Shields, and John Matthews |
A Verifying Core for a Cryptographic
Language Compiler [Paper] [Slides] |
|
| 9:30-10:00 | David Hardin, Eric Smith, and William Young |
A Robust Machine Code Proof Framework for Highly Secure Applications
[Paper] [Slides] |
|
| 10:00-10:30 | Break | Session 2, Chair: Jose Luis Ruiz-Reina | |
| 10:30-11:00 | John Cowles and Ruben Gamboa | Unique Factorization in ACL2: Euclidean Domains [Paper] |
|
| 11:00-11:30 | David Greve | Parameterized Congruences in ACL2 [Paper] [Slides] |
|
| 11:30-11:45 | Sol Swords and William Cook |
Soundness of the Simply Typed Lambda Calculus in ACL2 [Paper] [Slides] |
|
| 11:45-12:30 | Matt Kaufmann and J Strother Moore |
An Overview of Recent and Upcoming ACL2 Developments |
|
| 12:30-14:00 | Lunch break | Session 3, Chair: Matt Wilding | |
| 14:00-14:30 | Mike Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds |
An Embedding of the ACL2 Logic in HOL [Paper] [Slides] |
|
| 14:30-15:00 | Julien Schmaltz and Dominique Borrione |
Towards a Formal Theory of On Chip Communications in the ACL2 Logic [Paper] [Slides] |
|
| 15:00-15:15 | Jared Davis | Memories: Array-like Records for ACL2 [Paper] |
|
| 15:15-15:30 | Matt Kaufmann and J Strother Moore |
ACM Software System Award Remarks |
|
| 15:30-16:00 | Break | Session 4, Chair: Pete Manolios | |
| 16:00-16:45 | Tony Hoare Invited Speaker |
The Ideal of Verified Software [Paper] |
|
| 16:45-18:15 |
David Hardin, Tony Hoare, Gerard Holzmann, William B. Martin, and J Strother Moore, |
Panel: Grand Challenge Problems for the ACL2 Community [Slides] |
|
| 19:00-21:30 | Workshop Dinner | ||
|
Wednesday, August 16 Workshop, Day 2 | Session 5, Chair: Matt Kaufmann | ||
| 9:00-9:30 | Erik Reeber and Jun Sawada |
Combining ACL2 and an Automated Verification Tool to Verify a Multiplier [Paper] [Slides] |
|
| 9:30-10:00 | Ruben Gamboa and John Cowles | Implementing a Cost-Aware Evaluator for ACL2 Expressions [Paper] |
|
| 10:00-10:30 | Robert S. Boyer and Warren A. Hunt, Jr. |
Function Memoization and Unique Object Representation for ACL2 Functions [Paper] |
|
| 10:30-11:00 | Break | Session 6, Chair: Ruben Gamboa | |
| 11:00-11:15 | David L. Rager | Adding Parallelization Capabilities to ACL2 [Paper] [Slides] |
|
| 11:15-11:30 | Sandip Ray | Quantification in Tail-recursive Function Definitions [Paper] [Slides] |
|
| 11:30-11:45 | Warren A. Hunt, Jr. and Serita M. Nelesen |
Phylogenetic Trees in ACL2 [Paper] [Slides] |
|
| 11:45-12:00 | Matt Kaufmann and J Strother Moore |
Double Rewriting for Equivalential Reasoning in ACL2 [Paper] [Slides] |
Rump Session (Part of Session 6) |
| 12:00-12:05 | Bill Bevier and David Russinoff |
Formally Modeling the x86 Instruction Set Architecture |
|
| 12:05-12:10 | Warren Hunt | BDDs |
|
| 12:10-12:15 | Peter Dillinger, Pete Manolios, J Strother Moore, and Daron Vroon |
ACL2s: The ACL2 Sedan |
|
| 12:15-12:20 | J Strother Moore | Semi-Automatic Functional Instantiation |
|
| 12:20-12:25 | David Russinoff | A Unified Mathematical Theory of
Register-Transfer Logic and Computer Arithmetic |
|
| 12:25-12:30 | Matt Kaufmann, Pete Manolios, J Strother Moore, and Daron Vroon |
Adding Calling Context Graphs to ACL2 for Improved Termination Analysis |
|
| 12:30-14:00 | Lunch break | Session 7, Chair: David Russinoff | |
| 14:00-14:30 | Dale Vaillancourt, Rex Page, and Matthias Felleisen |
ACL2 in DrScheme [Paper] [Slides] |
|
| 14:30-15:00 | Jared Davis | Reasoning about ACL2 File Input [Paper] |
|
| 15:00-15:30 | Warren A. Hunt, Jr. and Erik Reeber |
A SAT-Based Procedure for Verifying Finite State Machines in ACL2 [Paper] [Slides] |
|
| 15:30-16:00 | Break | Session 8, Chair: Warren Hunt | Rump Session Start (Part of Session 8) |
| 16:00-16:05 | Jared Davis | Milawa: An Extensible Proof Checker for an ACL2-like Logic |
|
| 16:05-16:10 | Jun Sawada | A SUDOKU Solver using ACL2 and SixthSense |
|
| 16:10-16:15 | Eric Smith | Using ACL2 to Verify Java Programs |
Rump Session End |
| 16:15-17:00 | Matt Kaufmann, J Strother Moore, and All |
Discussion on Possible Future Enhancements to ACL2 |
|
| 17:00-17:30 | Pete Manolios, Matt Wilding, and All |
Business Meeting |
Workshop ends |