[Hol-info] ACL2 2006 Call For Participation

[Panagiotis M. <man...@cc...>]

                        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

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

10:30-11:00 	John Cowles and Ruben Gamboa
                Unique Factorization in ACL2: Part 1 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

14:00-14:30 	Erik Reeber and Warren A. Hunt, Jr.
                A SAT-Based Procedure for Verifying Finite State Machines in ACL2

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 	ACM Software System Award Session
                

15:30-16:00 	Break

Session 4

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

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

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 	TBA
                Rump Session

12:30-14:00 	Lunch break

Session 7

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 	Mike Gordon, Warren A. Hunt, Jr., Matt Kaufmann, and James Reynolds
                An Embedding of the ACL2 Logic in HOL

15:30-16:00 	Break

Session 8

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