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
http://www.cs.utexas.edu/~sandip/acl2-09/

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:

Applications of ACL2 in hardware and software system verification
Formalization of mathematics in ACL2
Use of ACL2 in emerging and novel application areas
New libraries, tools, and interfaces for ACL2
Connection of ACL2 with other formal (and semi-formal) verification tools
Foundational issues related to ACL2
Comparison of ACL2 with other formal verification tools
Reports and proposals on improvement of ACL2
Challenge problems related to implementation and applications of ACL2
Classroom and pedagogical experiences in the use of ACL2

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.

Organization

Organizing Committee

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

Program Committee

John Cowles, University of Wyoming, USA
Ruben Gamboa, University of Wyoming, USA
Mike Gordon, Cambridge University, UK
Matt Kaufmann, University of Texas at Austin, USA
Francisco Palomo Lozano, Universidad de Cádiz, Spain
Panagiotis Manolios, Northeastern University, USA
John Matthews, Galois, Inc., USA
J Strother Moore, University of Texas at Austin, USA
Rex Page, University of Oklahoma, USA
Jun Sawada, IBM Austin Research Laboratory, USA
Julien Schmaltz, Radboud University, Nijmegen, the Netherlands
Natarajan Shankar, SRI International, USA
Rob Sumners, Advanced Micro Devices, Inc., USA
Freek Wiedijk, Radboud University, Nijmegen, the Netherlands
Matt Wilding, Rockwell Collins, Inc.

Steering Committee

John Cowles, University of Wyoming, USA
Ruben Gamboa, University of Wyoming, USA
Matt Kaufmann, University of Texas at Austin, USA
Panagiotis Manolios, Northeastern University, USA
J Strother Moore, University of Texas at Austin, USA
Jun Sawada, IBM Austin Research Laboratory, USA
Matt Wilding, Rockwell Collins, Inc., USA

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

ACL2 2009 Call for Papers