[ forwarding on behalf of Sandip Ray <sandip@cs.utexas.edu> ] [ Apologies if you get several copies of this call for papers. Please share it with students and colleagues who may be interested in the workshop. ] =============================================================================== 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