A PDF version of the original Call for Papers is available here.

ACL2 2009
Call for Papers

Eighth International Workshop on the ACL2 Theorem Prover and Its Applications
May 11-12, 2009
Northeastern University, Boston, MA, USA

In cooperation with ACM SIGPLAN

Important Dates

Abstract Submission: January 12, 2009
Paper Submission: January 28, 2009
Acceptance Notification:      March 2, 2009
Final Version: March 31, 2009

Scope of Conference

ACL2 2009 is a major forum for the users of the ACL2 theorem proving system to present research related to the ACL2 theorem prover and its applications, and is the eighth in the series of workshops, occurring at approximately 18-month intervals. ACL2 is a state-of-the-art automated reasoning system, the latest in the Boyer-Moore family of theorem provers, for which its authors received the 2005 ACM Software Systems Award. ACL2 2009 is planned as a two-day workshop to be held in Boston, MA, USA, on May 11-12, 2009. In addition to paper presentations, ACL2 2009 is anticipated to include two keynote lectures, a panel discussion, and several rump sessions discussing ongoing research. We invite submission of papers on any topic related to ACL2 and its applications. We strongly encourage the participation of users of other theorem provers and researchers and practitioners interested in theorem proving technology. Appropriate topics include, but are not limited to, the following:

Paper Submission

Submissions must be made electronically in PDF format through the ACL2 2009 Web site. Submissions must use ACM SIG Proceedings format with letter-size paper (see URL http://www.acm.org/sigs/pubs/proceed/template.html). ACL2 2009 is organized in cooperation with ACM SIGPLAN and the proceedings are expected to be published in the ACM Digital Library. Two categories of papers will be accepted: long (at most 10 pages) and short (at most 4 pages). Authors may assume that the audience has a working knowledge of ACL2's syntax, basic commands, and modeling techniques. Papers should contain a short abstract of about 150 words, clearly stating the contribution of the submission. Papers should be self-contained, but we strongly encourage authors to follow the tradition (where applicable) of providing ACL2 "books", or script files, with instructions for their execution. For accepted papers, these books will be mirrored from the ACL2 Home Page and included in the future ACL2 distributions. At least one author of each accepted paper will be required to register for the workshop and present the paper.


Organizing Committee


Sandip Ray, University of Texas at Austin
David Russinoff, Advanced Micro Devices, Inc.
Local Arrangements
Panagiotis Manolios, Northeastern University
Ruben Gamboa, University of Wyoming

Program Committee

Steering Committee