The 2015 ACL2 Workshop will be held in Austin, Texas, USA, in conjunction with (and immediately following) FMCAD 2015. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. Keynote talks will be given by J Strother Moore and John O'Leary.
Here is link to a text file containing the email Call for Papers, which corresponds to the first two sections below.
Abstract submission: June 2, 2015 (formerly May 26) Paper submission: June 9, 2015 (formerly June 2) Author notification: July 17, 2015 Camera ready: August 17, 2015 Early registration ends: August 19, 2015 Workshop: October 1-2, 2015
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-2015 is a two-day workshop to be held in Austin, Texas, USA, on October 1-2, 2015. It is the 13th in the series of ACL2 workshops, which occur approximately every 18 months. The workshop will feature technical papers, keynote 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.
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=acl22015
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 types need short abstracts submitted by the "Abstract submission" deadline. Accepted submissions of both types will appear 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. Authors of long papers will have more time to present their work at the workshop. 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. We expect that the workshop proceedings will be published as a volume of Electronic Proceedings in Theoretical Computer Science (EPTCS). 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. We strongly encourage authors of such papers to provide ACL2 script files (aka "books") along with instructions for using these books in ACL2. Such supporting materials should be certifiable by running the following shell command in the directory of your contributed books, where ACL2_DIR denotes your ACL2 sources directory and ACL2 denotes your ACL2 executable.
ACL2_DIR/books/build/cert.pl --acl2 ACL2 *.lisp
For accepted papers, we will ask authors to make these books available by adding them to the ACL2 Community Books.
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 will be given priority when submitted earlier (more to come on this later).
The workshop will take place on the campus of the University of Texas in room 2.402 of POB (The Peter O'Donnell Jr. Building, formerly known as ACES), which is located on the corner of 24th Street and Speedway. Visitor parking is available in the parking garages, of which the San Jacinto Garage is closest to POB.
UPDATE: The block of rooms has been mostly released at the Austin Folk House Bed and Breakfast (see below), but a few rooms may still be available. Another option to consider at this point is the DoubleTree Hilton UT area, where a block of rooms is being held for FMCAD (and can be reasonably expected to honor the ACL2 Workshop as well).
A block of rooms has been set aside at the Austin Folk House Bed and Breakfast, which is within walking distance of the workshop venue at the University of Texas. Here are details, where room rates do not include taxes.
Wed., Sep. 30: $105/night (FMCAD and/or ACL2 Workshop) Thu., Oct. 1: $105/night (ACL2 Workshop) Fri., Oct. 2: $240/night (ACL2 Workshop)
The blocks will be held until August 22 (see UPDATE above), but rooms might be rented out long before then. This fall is a busy time in Austin, with the Austin City Limits festival (ACL Music Festival) starting Oct. 2. Note that on Sept. 30 (the night before the ACL2 Workshop begins), we share the block with FMCAD, which could fill up that block for that night.
The Friday night price is high because of the ACL Music Festival (see above). Still, the average over three nights is quite reasonable for a major city like Austin. So we plan that the workshop will end at approximately 6:00 pm Friday, and some visitors will stay overnight on Friday.
NOTE for UT students: scholarships are available for covering the registration fee. If you are interested, follow these links to the scholarship flyer and the scholarship application form.
The program schedule is available.
The proceedings are available both in HTML format and as a PDF file.
Program highlights include the following (but see the links just above for details).