11-12 May 2009
Boston MA, U.S.A.
===============================================================================
CALL FOR PAPERS
===============================================================================
ACL2 2009
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 19, 2009
Acceptance Notification: February 23, 2009
Final Version: March 23, 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
application, 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
Co-Chairmen: Sandip Ray, University of Texas at Austin, USA
David Russinoff, Advanced Micro Devices, Inc., USA
Local Arrangements: Panagiotis Manolios, Northeastern University, USA
Publications: Ruben Gamboa, University of Wyoming
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
==============================================================================
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 Cadiz, 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., USA