ACL2 2006
Sixth International Workshop on the ACL2 Theorem Prover and its Applications
Seattle, Washington, USA
August 15 - 16

The proceedings for ACL2 2006 are now available online for $9.99, at

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
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
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
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
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
10:00-10:30 Robert S. Boyer and
Warren A. Hunt, Jr.
Function Memoization and Unique Object Representation for ACL2 Functions
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
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
Discussion on Possible Future Enhancements to ACL2
17:00-17:30 Pete Manolios,
Matt Wilding, and
Business Meeting
Workshop ends