[TYPES/announce] ACL2-2020 - May 28-29, 2020 - Call for Papers

[Grant Olney Passmore]

ACL2 2020 - Call for Papers
16th International Workshop on the ACL2 Theorem Prover and Its Applications
May 28-29, 2020. Austin, Texas, USA.

The 2020 ACL2 Workshop will be held in Austin, Texas, USA. We invite ACL2 users,
experts and beginners alike, users of other theorem provers, and persons
interested in the applications of theorem proving technology to submit papers to
the Workshop.

* Important Dates

Abstract Submission: December 22, 2019
Paper Submission: January 12, 2020
Author Notification: March 8, 2020
Camera-Ready Copy: April 12, 2020
Workshop: May 28-29, 2020

* Website

More information may be found at: http://acl2-2020.info

* 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-2020 is a two-day workshop to be held in Austin, Texas, USA, on May 28-29,
2020. It is the 16th in the series of ACL2 workshops, which occur approximately
every 18 months. The workshop will feature invited keynotes, technical papers,
and rump sessions that discuss ongoing research.

We invite submissions of papers on any topic related to ACL2 and its
applications. We strongly encourage submissions from new members of the ACL2
community, including graduate students and researchers who are primarily
involved with other theorem provers or formal methods. 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. and they should be
prepared in the EPTCS templates, available from http://style.eptcs.org. All
papers must be submitted via EasyChair at
https://easychair.org/my/conference?conf=acl2-2020.

The ACL2 Workshop accepts both long papers (up to sixteen pages) and extended
abstracts (up to two pages). Both categories of papers will require short
abstracts to be submitted by the "Abstract submission" deadline and will be
refereed by at least two members of the program committee. Accepted submissions
in both categories will be included in the final workshop proceedings, although
speaking slots will be shorter for extended abstracts. At least one author of
each accepted submission 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 interested
readers can pursue the abstract topic. Long papers and extended abstracts must
describe work that has already been done, not simply ideas for future work.
Current and planned (or suggested) work may be presented in the Rump Session.

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). Long papers will be published as PDFs, and
extended abstracts will be published as HTML snippets. Please see the EPTCS
copyright page (http://copyright.eptcs.org/) for a discussion of licensing.
Please also see the EPTCS LaTeX style file and formatting instructions
(http://style.eptcs.org).

Many papers presented at the workshop will describe interactions with the
theorem prover. Authors of such papers are required to provide ACL2 script files
(typically, ACL2 books) along with instructions for their use with ACL2, unless
they provide a small text file explaining why supporting materials are not
appropriate (e.g., for a theory paper). Such supporting materials should have
proper licenses and copyrights (feel free to email the workshop chairs if you
have questions about that). The books should be certifiable either with custom
instructions that are clearly provided, or by running the following shell
command in the directory of your contributed books, where $ACL2_DIR denotes your
ACL2 sources directory and ACL2 denotes a recent ACL2 executable: prompt%
$ACL2_DIR/books/build/cert.pl --acl2 ACL2 *.lisp

Send the supporting materials to Ruben Gamboa, ruben at uwyo.edu. The authors can
expect the reviewers to take the supporting materials into account during the
refereeing process.

Authors of accepted papers are required to make these ACL2 books available by
adding them to the ACL2 Community Books. (The chairs may assist in that process,
if asked.)

* Rump Sessions

The workshop will also feature "rump sessions," in which participants can
describe ongoing or proposed research related to ACL2. Proposals for rump
session presentations, including a title and short abstract, may be accepted
until the workshop, but preference will be given to early submissions and
subject to available time. Rump session proposals should be sent to our
ACL2-2020 EasyChair email address: acl22020 at easychair.org

* Programme Committee

Cuong Chau, Arm, Inc.
John Cowles, University of Wyoming
Shilpi Goel, Centaur Technology, Inc.
Mark Greenstreet, The University of British Columbia
David Hardin, Collins Aerospace
Warren Hunt, The University of Texas at Austin
Matt Kaufmann, The University of Texas at Austin
Eric McCarthy, Kestrel Institute
Mihir Mehta, The University of Texas at Austin
Yan Peng, The University of British Columbia
David Rager, Oracle Corp.
Sandip Ray, University of Florida
Jose-Luis Ruiz-Reina, University of Seville
Anna Slobodova, Centaur Technology, Inc.
Eric Smith, Kestrel Institute
Rob Sumners, Centaur Technology, Inc.
Sol Swords, Centaur Technology, Inc.

* Workshop Co-Chairs

Ruben Gamboa, University of Wyoming
Grant Passmore, Imandra Inc.

* Steering Committee

J Strother Moore, The University of Texas at Austin
Matt Kaufmann, The University of Texas at Austin
Shilpi Goel, Centaur Technology, Inc.
Warren Hunt, The University of Texas at Austin
Anna Slobodova, Centaur Technology, Inc.

* Local Arrangements

Emily Gamboa, Rice University