Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ACL2 2018: Second Call for Papers

view this post on Zulip Email Gateway (Aug 22 2022 at 17:34):

From: Alessandro Coglio <coglio@kestrel.edu>
Second Call for Papers:
ACL2 2018
15th International Workshop on the ACL2 Theorem Prover
and Its Applications

November 5-6, 2018, Austin, Texas, USA

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

The 2018 ACL2 Workshop will be held in Austin, Texas, USA, and it is
co-located with FMCAD (http://www.fmcad.org/FMCAD18). 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: June 30, 2018
Paper submission: July 7, 2018
Author notification: August 25, 2018
Camera ready: September 25, 2018
Workshop: November 5-6, 2018

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-2018 is a two-day workshop to be held in Austin, Texas, USA, on
November 5-6, 2018, immediately after FMCAD
(http://www.fmcad.org/FMCAD18), on the University of Texas campus.
It is the 15th in the series of ACL2 workshops, which occur
approximately every 18 months. The workshop will feature technical
papers as well as rump sessions that discuss ongoing research.

There will be three invited keynote talks, given by:

Sandip Ray, University of Florida at Gainesville
Alastair Reid, ARM
Sol Swords, Centaur Technology

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. Submissions
should be prepared in the EPTCS templates, available from
http://style.eptcs.org <http://style.eptcs.org/>, and submitted via
EasyChair. See the ACL2 2018 website for details.

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
someone can pursue the abstract topic. Like long papers, extended
abstracts 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). 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.

ACL2_DIR/books/build/cert.pl --acl2 ACL2 *.lisp

Send the supporting materials to Matt Kaufmann,
kaufmann@cs.utexas.edu.

For accepted papers, we will require authors to make these books
available by adding them to the ACL2 Community Books. (The chairs
may assist in that process, if asked.) The authors can expect the
reviewers to take the supporting materials into account during the
refereeing process.

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 workshop, but preference will
be given to early submissions and subject to available time.

ORGANIZATION:

Chairs

Shilpi Goel (Centaur Technology, Inc.)
Matt Kaufmann (University of Texas)

Program Committee

Harsh Chamarthi (General Electric)
Alessandro Coglio (Kestrel Institute)
Jared Davis (Apple)
Ruben Gamboa (University of Wyoming)
Shilpi Goel (Centaur Technology, Inc.)
Dave Greve (Rockwell-Collins, Inc.)
Warren Hunt (University of Texas at Austin)
Sebastiaan Joosten (University of Twente)
Matt Kaufmann (University of Texas)
John O'Leary (Intel)
Grant Passmore (Aesthetic Integration)
David Rager (Oracle, Inc.)
Sandip Ray (University of Florida)
David Russinoff (ARM, Ltd.)
Julien Schmaltz (Eindhoven University of Technology)
Anna Slobodova (Centaur Technology, Inc.)
Eric Smith (Kestrel Institute)
Sol Swords (Centaur Technology, Inc.)

The chairs thank Mertcan Temel for his assistance with local arrangements.

NOTE:

Please see the website

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

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

Note that no block of rooms is being reserved for the workshop.
Please see the following link
http://www.cs.utexas.edu/users/moore/acl2/workshop-2018/index.html#lodging
for information about lodging options near the workshop venue.

HISTORICAL INFORMATION:

The ACL2 Workshop series has previously published with EPTCS in 2011,
2013, 2014, 2015, and 2017. In other past years: the proceedings
were published with Springer LNCS 6172 in 2010, and ACM digital
library in 2006 and 2009. The first ACL2 workshop in 1999 resulted
in two books:

ACL2 workshops have been co-located with major conferences in formal
methods in the past: European Joint Conferences on Theory and
Practice of Software (ETAPS) in 2002, Computer-Aided Verification
(CAV) in 2003, Federated Logic Conference (FLoC) in 2006, 2010, and
2014, and Formal Methods in Computer-Aided Design (FMCAD) in 2004,
2007, 2011, 2015, and 2018.

Last updated: Nov 21 2024 at 12:39 UTC