The 2018 ACL2 Workshop will be held in Austin, Texas, USA, immediately after FMCAD. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend.
Here is a link to a text file containing an email Call for Papers, corresponding to the first two sections below.
Abstracts submission: July 7, 2018 [no further extension anticipated] Paper submission: July 14, 2018 [no further extension anticipated] Author Notification: August 25, 2018 Camera-ready (author) September 25, 2018 Workshop: November 5-6, 2018
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, 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:
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.
Submissions must be made electronically in PDF format. Submissions should be prepared in the EPTCS templates, available from http://style.eptcs.org, and submitted via EasyChair at:
https://easychair.org/conferences/?conf=acl22018
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 need short abstracts submitted by the "Abstract submission" deadline. 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 for a discussion of licensing. Please also see the EPTCS LaTeX style file and formatting instructions.
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 or (as discussed above) a small
explanatory text file 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 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, should be sent to the chairs at acl22018@easychair.org. These proposals may be accepted until the workshop, but preference will be given to early submissions and subject to available time.
Feel free to email the program chairs if you have questions.
The chairs thank Mertcan Temel for his assistance.
The workshop will take place on the campus of the University of Texas in the Gates Dell Complex (GDC), North Wing, Room 6.302 (Faculty Lounge), which is located south of 24th Street on Speedway. Visitor parking is available in the parking garages, of which the San Jacinto Garage is closest to GDC.
The room has a laptop projector that should support native 1920x1200 resolution, as well as most standard HD (16:9) resolutions, and quite possibly 4:3 as well.
Here are some possibilities. Note that no block of rooms is being reserved.
Register for ACL2-2018 at the following website:
https://www.regonline.com/acl2-2018Registration fees are as follows.
Follow this link to the program, which has information on the Sunday welcome reception, Monday conference dinner, workshop location, and parking, as well as a schedule of talks. Note that the schedule of talks may change.
Proceedings (EPTCS 280) are available online.
Note: For the PDF version, to ensure perfect centering on A4 paper when printing from acroread, use:
- Page Scaling: None
- Auto Rotate and Center