Email Gateway (Aug 18 2022 at 09:26): Email Gateway (Aug 18 2022 at 09:26):From: Panagiotis Manolios <manolios@cc.gatech.edu>
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
Last updated: Nov 21 2024 at 12:39 UTC