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

PDF Version of the Call for Papers

			       ACL2 2006
 International Workshop on the ACL2 Theorem Prover and its Applications


	       August 15-16, 2006 in Seattle, Washington
       Part of FLoC 2006 (
		   Hosted by CAV 2006 and IJCAR 2006

Abstract Submission Deadline	April 14, 2006, 11:59 PM NY time
Paper Submission Deadline	April 19, 2006, 11:59 PM NY time
Acceptance notification:    	June 9, 2006
Final version due:		July 24, 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.  ACL2 2006 is hosted by the CAV
and IJCAR conferences, which are part of FLoC 2006, the Federated Logic
Conference.  In addition, and as reflected by our program committee, we
encourage participation from users of other theorem provers and persons
interested in the application of theorem proving technology.  We invite
papers on any ACL2-related topic, including but not limited to:

+ applications of the theorem prover,

+ proposals for ACL2 theorem prover improvements, especially as
  illustrated in experimental extensions or other systems,

+ comparisons with other theorem provers, programming languages, or
  specification languages,

+ solved (and unsolved!) challenge problems, and

+ implementations connecting ACL2 with other systems.

Submissions must be made electronically in PDF format, following the
instructions on the ACL2 2006 Web site.  Submissions must use the ACM
SIG Proceedings format with letter-size paper (see

Two categories of papers will be accepted: long (at most 10 pages) and
short (at most 4 pages). Note that the current paper format is much more
compact than the LNCS format we used in the past! Authors can assume
that the workshop audience has a working knowledge of ACL2's syntax,
basic commands, and modeling techniques.  Papers should contain a short
abstract of approximately 150 words clearly stating the contribution of
the submission.  Authors of accepted papers are required to give a
presentation at the workshop.  Papers should be self-contained, but, as
has been the case traditionally (and where applicable), we strongly
encourage authors to provide ACL2 "books" or script files that provide
full details, along with instructions for how to process these books
with ACL2.  The submission guidelines for supporting materials, which we
strongly recommend you adhere to can be found at  For
accepted papers, these books will be mirrored on the ACL2 home page and
included in future ACL2 distributions. We expect to provide workshop
proceedings and to include these proceedings in the ACM digital library.

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

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