[TYPES/announce] ACL2'14: Call for papers

[Verbeek, Freek]

                     *** CALL FOR PAPERS ***


                               ACL2 2014
          International Workshop on the ACL2 Theorem Prover
                         and its Applications
                         in cooperation with
                              ACM SIGPLAN

               July 12-13, 2014 in Vienna, Austria

                          http://vsl2014.at/acl2/

                              CALL FOR PAPERS

IMPORTANT DATES

Abstract Submission    30th March2014
Paper Submission       6th April 2014
Author Notification    11th May 2014
Camera Ready           25th May 2014


WORKSHOP SCOPE

ACL2 2014 is the major technical forum for users of the ACL2 theorem
proving system to present research related to the ACL2 theorem prover
and its applications. ACL2 2014 is the eleventh in the series of ACL2
workshops, which occur approximately every 18 months. ACL2 is an
industrial-strength automated reasoning system, the latest in the
Boyer-Moore family of theorem provers. The 2005 ACM Software System
Award was awarded to Boyer, Kaufmann, and Moore for their work in ACL2
and the other theorem provers in the Boyer-Moore family.

ACL2 2014 is a two-day workshop to be held in Vienna, Austria.
The workshop will feature technical papers, invited
talks, and rump sessions discussing ongoing research. We invite
submissions of papers on any topic related to ACL2 and its
applications, and we strongly encourage submissions related to other
theorem provers or formal methods that are of interest to the ACL2
community. Suggested topics include but are not limited to the
following:

    * software or hardware verification with ACL2,
    * formalizations of mathematics in ACL2,
    * new libraries, tools, and interfaces for ACL2,
    * novel uses of ACL2,
    * experiences with ACL2 in the classroom,
    * reports of and proposals for improvements of ACL2,
    * comparisons with other theorem provers,
    * comparisons with other programming or specification languages,
    * challenge problems and their solutions,
    * foundational issues related to ACL2, and
    * implementations connecting ACL2 with other systems.

PAPER SUBMISSIONS

Submissions must be made electronically in PDF format, as directed in
the ACL2 2014 website. Submissions should be prepared in the EPTCS
templates, available from http://style.eptcs.org.

The ACL2 Workshop accepts both long papers (up to sixteen pages) and
extended abstracts (up to two pages). Both categories of papers will
be fully refereed, but only long papers will be included in the final
workshop proceedings. At least one author of each accepted papers must
register for the workshop and give a presentation summarizing the
paper's results. Authors of long papers will have more time to present
their work at the workshop. One of the main advantages of the ACL2
Workshop is that attendees are already knowledgeable about ACL2, its
syntax, its basic commands, and the art of writing models in it. So
authors may assume that readers have this familiarity. The workshop
proceedings will be published as a volume of Electronic Proceedings in
Theoretical Computer Science (EPTCS).

Many papers presented at the workshop will describe interactions with
the theorem prover. We strongly encourage authors of such papers to
provide ACL2 script files (aka "books") along with instructions for
using these books in ACL2. Such supporting materials should follow the
guidelines at
http://www.cs.utexas.edu/users/moore/acl2/books/index.html. For
accepted papers, we will ask authors to make these books available
by adding them to the ACL2 books repository.

The workshop will also feature ``rump sessions'', in which
participants can describe ongoing research related to ACL2. Proposals
for rump session presentations, including a title and short abstract,
will be accepted until the workshop.

ORGANIZATION

    Chairs

        Freek Verbeek, Open University of The Netherlands
        Julien Schmaltz, Eindhoven University of Technology, The Netherlands

    Program Committee

    John Cowles (University of Wyoming)
    Warren Hunt (University of Texas at Austin)
    Matt Kaufmann (University of Texas at Austin)
    Panagiotis Manolios (Northeastern University)
    Magnus O. Myreen (University of Cambridge)
    Lee Pike (Galois, Inc.)
    David Rager (Oracle, Inc.)
    Sandip Ray (Intel Corporation)
    Jose Luis Ruiz Reina (University of Seville)
    David Russinoff (Intel Corp.)
    Eric Smith (Stanford University)
    Sol Swords (Centaur Technology, Inc.)
    Laurent Théry (INRIA)
    Makarius Wenzel (Université Paris-Sud)
    Freek Wiedijk (Radboud University Nijmegen)


Deze e-mail is uitsluitend bestemd voor de geadresseerde(n). Verstrekking aan en gebruik door anderen is niet toegestaan. Open Universiteit sluit iedere aansprakelijkheid uit die voortvloeit uit elektronische verzending. Aan de inhoud van deze e-mail en/of eventueel toegevoegde bijlagen kunnen geen rechten worden ontleend.

This e-mail is intended exclusively for the addressee(s), and may not be passed on to, or made available for use by any person other than the addressee(s). Open Universiteit rules out any and every liability resulting from any electronic transmission. No rights may be derived from the contents of this message.