[FOM] ACL2 2009: Final Call for Papers

[Sandip Ray]

[ 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. ]

===============================================================================
                         FINAL 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
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

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