*** 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 . 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.