CALL FOR PARTICIPATION
ACL2 2006
International Workshop on the ACL2 Theorem Prover and its Applications
In-cooperation with ACM SIGPLAN and ACM SIGSOFT
http://www.cc.gatech.edu/~manolios/acl206
August 15-16, 2006 in Seattle, Washington
Part of FLoC 2006 (http://research.microsoft.com/floc06/)
Hosted by CAV 2006 and IJCAR 2006
------------------------------------------------
Early Registration Deadline: July 10, 2006
Regular Registration Deadline: August 1, 2006
Hotel Registraion Deadline: July 21, 2006
------------------------------------------------
ACL2 2006 is the major technical forum for users of the ACL2 theorem
proving system and is the sixth in a series of workshops that occur
every 18 months. ACL2 is an industrial-strength automated reasoning
system that is part of the Boyer-Moore family of theorem provers,
winner of the 2005 ACM Software System Award.
Invited Talk
========================================================================
Tony Hoare (Microsoft Research)
The Ideal of Verified Software
Panel
========================================================================
David Hardin, Tony Hoare, Gerard Holzmann, J Strother Moore, ...
Grand Challenge Problems for the ACL2 Community
Program
========================================================================
Tuesday, August 15
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
9:30-10:00 David Hardin, Eric Smith, and William Young
A Robust Machine Code Proof Framework for Highly Secure Applications
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
11:30-11:45 Sol Swords and William Cook
Soundness of the Simply Typed Lambda Calculus in ACL2
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
14:30-15:00 Julien Schmaltz and Dominique Borrione
Towards a Formal Theory of On Chip Communications in the ACL2 Logic
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 Invited Speaker: Tony Hoare
The Ideal of Verified Software
16:45-18:15 David Hardin, Tony Hoare, Gerard Holzmann, J Strother Moore, ...
Panel: Grand Challenge Problems for the ACL2 Community
19:00-21:30 Workshop Dinner
Wednesday, August 16
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
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, Ruben Gamboa
11:00-11:15 David L. Rager
Adding Parallelization Capabilities to ACL2
11:15-11:30 Sandip Ray
Quantification in Tail-recursive Function Definitions
11:30-11:45 Warren A. Hunt, Jr. and Serita M. Nelesen
Phylogenetic Trees in ACL2
11:45-12:00 Matt Kaufmann and J Strother Moore
Double Rewriting for Equivalential Reasoning in ACL2
12:00-12:30 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, David Russinoff
14:00-14:30 Dale Vaillancourt, Rex Page, and Matthias Felleisen
ACL2 in DrScheme
14:30-15:00 Jared Davis
Reasoning about ACL2 File Input
15:00-15:30 Erik Reeber and Warren A. Hunt, Jr.
A SAT-Based Procedure for Verifying Finite State Machines in ACL2
15:30-16:00 Break
Session 8, Warren Hunt
16:00-17:45 Matt Kaufmann, J Strother Moore, and All
Discussion on Possible Future Enhancements to ACL2
16:45-17:30 Pete Manolios, Matt Wilding, and All
Business Meeting
ORGANIZATION
========================================================================
Chairs: Panagiotis Manolios, Georgia Institute of Technology
Matthew Wilding, Rockwell Collins Inc.
Publications: Ruben Gamboa, University of Wyoming
Webmasters: Sudarshan Srinivasan, Georgia Tech
Daron Vroon, Georgia Tech
PROGRAM COMMITTEE
========================================================================
Ruben Gamboa, University of Wyoming, USA
David Greve, Rockwell Collins Inc., USA
Warren Hunt, University of Texas at Austin, USA
Deepak Kapur, University of New Mexico, USA
Matt Kaufmann, University of Texas at Austin, USA
Bill Legato, NSA, USA
Panagiotis Manolios, Georgia Institute of Technology, USA
Jose Meseguer, University of Illinois at Urbana-Champaign, USA
Paul Miner, NASA Langley Research Center, USA
J Strother Moore, University of Texas at Austin, USA
Lawrence C. Paulson, University of Cambridge, UK
Jose Luis Ruiz-Reina, University of Seville, Spain
David M. Russinoff, Advanced Micro Devices, Inc., USA
Jun Sawada, IBM Austin Research Laboratory, USA
Mary Sheeran, Chalmers University of Technology, Sweden
Konrad Slind, University of Utah, USA
Matthew Wilding, Rockwell Collins Inc., USA
Sixth International Workshop on the ACL2 Theorem Prover and its Applications
Seattle, Washington, USA
August 15 - 16