The 2023 ACL2 Workshop will be held in Austin, Texas, USA and also online, on November 13-14, 2023. The extent of in-person activities will be determined by the status of the pandemic, but there will be online support for all presentations. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend.
Abstract submission: July 15 (formerly July 8)
Paper submission: July 22 (formerly July 15)
Author Notification: September 9 (formerly September 2)
Camera-ready (author): October 3
Workshop: November 13-14 (reception November 12)
See the Program for the workshop
schedule, including locations and time for the reception on Sunday,
November 12 and the conference dinner on Monday, November 13.
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-2023 is planned to be a two-day workshop to be held in Austin, Texas, USA, on November 13-14, 2023. The workshop is planned to be held in-person on the University of Texas at Austin campus. In addition to in-person participation, the workshop will support online participation for all talks and presentations. The workshop will be the 18th 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 two 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=acl22023
The ACL2 Workshop accepts both regular papers (up to sixteen pages excluding references) and extended abstracts (up to three pages excluding references). 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. The presentation of the paper by the author may be done in-person or online.
Extended abstracts should contain at least one or two references so someone can pursue the abstract topic. Like regular 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; please check back later for details.
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; or, you can explain where to find supporting
materials that are already in the commmunity books). 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 either Alessandro
Coglio (coglio@kestrel.edu)
or Sol Swords (sswords@gmail.com).
For accepted papers, we will require authors to make these books available by adding them to the ACL2 Community Books. (Matt Kaufmann 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. 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 Organizing Chairs if you have questions.
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.
In addition, the workshop will be held online. Details of the online participation will be forthcoming.
Here are some possibilities. Note that no block of rooms is being reserved.
Visit the ACL2-2023 registration website
at https://acl2.regfox.com/acl2-workshop-2023,
which shows fees of $0 to $140 for various categories (student,
professional, and online only with or without
banquet/t-shirt).
Note that the discounted fees for early
registration end after October 31.
Follow this link to the program, which has information on the schedule of talks and workshop location. Note that the schedule of talks may change.
Proceedings for the workshop are available on the EPTCS website in pdf format and html format.
You can also view the supporting materials for the workshop papers in
the ACL2 github repo. The supporting materials will be in
the books/workshops/2023
directory unless otherwise specified. Please see the
README file in
the workshop books directory for further information on locating supporting materials per paper.
BEST STUDENT PAPER AWARDS
Congratulations to winners of the best student paper awards, listed below. These were given to student authors of the best papers written solely or primarily by a student.
We are grateful to our sponsors (listed below)!