*** 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.
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
