The Coq mailing list

[hunt AT cs.utexas.edu (Warren A. Hunt Jr.)]

                    *** SECOND CALL FOR PAPERS ***

                              ACL2 2017
        14th International Workshop on the ACL2 Theorem Prover
                         and Its Applications

                 May 22-23, 2017, Austin, Texas, USA

  http://www.cs.utexas.edu/users/moore/acl2/workshop-2017/index.html

 The 2017 ACL2 Workshop will be held in Austin, Texas, USA.  We invite
 users of ACL2, users of other theorem provers, and persons interested
 in the applications of theorem proving technology to attend.

 IMPORTANT DATES:

 Abstract submission:   January 18, 2017
 Paper submission:      January 25, 2017
 Author notification:   March 7, 2017
 Camera ready:          April 3, 2017
 Workshop:              May 22-23, 2017

 AIMS AND SCOPE:

 The ACL2 Workshop series 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 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 2017 is a two-day workshop to be held in Austin, Texas, USA, on
 May 22-23, 2017, on the University of Texas campus.  It is the 14th
 in the series of ACL2 workshops, which occur approximately every 18
 months.  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 new results in the following
 areas.

     * Software or hardware verification with ACL2
     * Formalizations of mathematics in ACL2
     * Libraries and tools for ACL2
     * User 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
     * Implementations connecting ACL2 with other systems

 PAPER SUBMISSIONS:

 Submissions must be made electronically in PDF format, as directed in
 the ACL2 2017 website. Submissions should be prepared in the EPTCS
 templates, available from http://style.eptcs.org
 <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, and both categories of papers will be included in
 the final workshop proceedings.  At least one author of each accepted
 paper must register for the workshop and give a presentation
 summarizing the paper's results.  Extended abstracts should contain
 at least one or two references so someone can pursue the abstract
 topic.  Like long papers, extended abstract must describe work that
 has already been done -- it is not for ideas for future work.  To
 discuss future work, we will have a rump session, and we will later
 appeal for those topics.

 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.  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, may be accepted until the beginning workshop, but a
 preference will be given to early submissions and subject to
 available time.

 ORGANIZATION:

     Chairs

     Warren Hunt (University of Texas)
     Anna Slobodova (Centaur Technology)

     Local Arrangements

     Mihir Metha (University of Texas)

     Program Committee

     Alessandro Coglio (Kestrel Institute)
     John Cowles (University of Wyoming)
     Mark Greenstreet (University of British Columbia)
     David Hardin (Rockwell-Collins, Inc.)
     Matt Kaufmann (University of Texas at Austin)
     Panagiotis Manolios (Northeastern University)
     J Strother Moore (University of Texas)
     Dmitry Nadezhin (Oracle, Inc.)
     Rex Page (University of Oklahoma)
     David Rager (Oracle, Inc.)
     Sandip Ray (NXP, Inc.)
     Jose Luis Ruiz Reina (University of Seville)
     David Russinoff (ARM, Ltd.)
     Rob Sumners (Centaur Technology, Inc.)
     Freek Verbeek (Open University of The Netherlands)

 NOTE:

 Please see the website

 http://www.cs.utexas.edu/users/moore/acl2/workshop-2017/index.html

 for further information including paper submission, organization,
 venue, lodging, and eventually, registration and program information.