ACL2 Workshop 2013

Other formats: Text | PDF

ACL2 2013

International Workshop on the ACL2 Theorem Prover and its Applications
May 30-31, 2013 in Laramie, WY, USA
http://www.cs.uwyo.edu/~ruben/acl2-13

CALL FOR PAPERS

IMPORTANT DATES

WORKSHOP SCOPE

ACL2 2013 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 2013 is the eleventh in the series of ACL2 workshops, which occur approximately every 18 months. 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 2013 is a two-day workshop to be held in Laramie, WY, USA on May 30-31, 2013. 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 the following:

• software or hardware verification with ACL2,
• formalizations of mathematics in ACL2,
• new libraries, tools, and 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, and
• 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, and submitted via EasyChair.

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, but only long papers will be included in the final workshop proceedings. At least one author of each accepted papers 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. 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. Such supporting materials should follow the guidelines at http://www.cs.utexas.edu/users/moore/acl2/books/index.html. 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, will be accepted until the workshop.

ORGANIZATION

Program Chairs

• Ruben Gamboa, University of Wyoming, USA
• Jared Davis, Centaur, USA

Program Committee

• Carl Eastlund, Northeastern University, USA
• David Greve, Rockwell Collins, USA
• Warren Hunt, University of Texas, USA
• Matt Kaufmann, University of Texas, USA
• Hanbing Liu, AMD, USA
• Panagiotis Manolios, Northeastern University, USA
• Magnus Myreen, University of Cambridge, UK
• David Rager, Battelle Memorial Institute, USA
• Sandip Ray, Intel, USA
• Jose Luis Ruiz Reina, University of Seville, Spain
• David Russinoff, Intel, USA
• Jun Sawada, IBM, USA
• Julien Schmaltz, Open University of the Netherlands, The Netherlands
• Konrad Slind, Rockwell Collins, USA
• Sol Swords, Centaur, USA
• Laurent Thery, INRIA, France

edit SideBar