[TYPES/announce] Call for Papers ACL2 2011

[Freek Wiedijk]

                          Call for Papers
 ACL2 2011: 10th International Workshop on the ACL2 Theorem Prover
                          and Its Applications
             3-4 November 2011, Austin, TX, USA
                 http://www.cs.ru.nl/~julien/acl2-11/

                            -----

Important dates
------------

Abstract submission: 13 June2011
Paper submission: 20 June 2011
Author notification: 25 July 2011
Final version: 02 September 2011


Scope of the workshop
------------------

ACL2 2011 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. ACL2 2011 is the tenth 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 2011 is planned as a two-day workshop to be held in Austin, TX, USA,
on 3-4 November 2011. ACL2 2011 is affiliated with FMCAD 2011, the
eleventh International Conference on Formal Methods in Computer Aided
Design (http://www.cs.utexas.edu/users/ragerdl/fmcad11/). In addition to paper
presentations, ACL2 2011 is anticipated to include 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.


Paper categories
-------------

Papers presented at the workshop will be assigned to one of the following
categories. At the time of submission, please indicate to which category you
think your paper belongs. If you are not sure about the category for your
paper, simply submit the paper to the "Other" category.

** Wizard spells ** (new)

Let the wizards reveal their spells!  Wizard spell papers must present
detailed proof techniques. They illustrate the use of ACL2 features, general
proof patterns, and advanced proof strategies. The objectives are to help
new users, to share the expertise of ACL2 "power users", and hopefully to inspire
and help other users.

** Applications **

Applications have played an important role in the development of ACL2.  ACL2
2011 welcomes papers reporting about user experiences in hardware and software
verification, formalization of mathematics, teaching, but also in emerging or
novel areas.

** What's new ? **

Papers of this category will present updates about the ACL2 systems and related
systems, like ACL2s, ACL2(r) or ACL2(h). Papers may present new system capabilities,
features, or interfaces.

** Other **

All papers that do not fit in any of the above categories belong to this category.

** Short and long papers **

In all categories, ACL2 2011 welcomes long (10 pages) and short (4 pages) papers.


Paper submission
--------------

Submissions must be made electronically in PDF format through Easy Chair.
The corresponding webpage can be found on the ACL2 2011 website.
Submissions must use ACM SIG Proceedings format with letter-size paper
(see http://www.acm.org/sigs/pubs/proceed/template.html). The
proceedings are expected to be published in the ACM Digital Library (pending).
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. Authors of accepted papers
are expected to present their papers at the conference and will be required to
sign copyright release forms. All submissions must be written in English.

Important dates AOE (Anywhere On Earth)
--------------------------------

Abstract Submission: 13 June 2011
Paper Submission: 20 June 2011
Author Notification: 25 July 2011
Final Version: 02 September 2011
Workshop:  03-04 November 2011


Web page
--------
http://www.cs.ru.nl/~julien/acl2-11/


Conference co-chairs
-----------------

David S. Hardin (Rockwell Collins)
Julien Schmaltz (Open University of the Netherlands)

Program Committee
----------------

John Cowles  (Univ. Wyoming, USA)
Mike Gordon (Cambridge Univ., UK)
David Greve (Rockwell Collins, USA)
David Hardin (Rockwell Collins, USA)
Warren Hunt (UT Austin, USA)
Matt Kaufmann (UT Austin, USA)
Panagiotis Manolios (Northeastern Univ., USA)
Francisco-Jesus Martin-Mateos (Univ. of Sevilla, Spain)
John Matthews (Galois, USA)
Cesar Munoz (NASA, USA)
Rex Page  (Univ. of Oklahoma, USA)
Laurence Pierre  (TIMA Labs., France)
Sandip Ray (UT Austin, USA)
David Russinoff (AMD, USA)
Jun Sawada (IBM, USA)
Julien Schmaltz (Open Universiteit, The Netherlands)
Natarajan Shankar (SRI, USA)
Sol Swords (Centaur, USA)
Freek Wiedijk (Radboud Univ. Nijmegen, The Netherlands)