ACL2 2022 - Final Call for Papers 17th International Workshop on the ACL2 Theorem Prover and Its Applications May 26-27, 2022. Austin, TX, USA and Online. Note: due to the ongoing pandemic and the uncertainty of conditions for travel and in-person participation going into May of this year and the need for attendees to plan accordingly, we (the chairs) want to notify everyone that unless conditions change dramatically and quickly, it is likely that the ACL2 workshop will be an online-only event. We will update the ACL2 workshop webpage with more details as they develop and as final decisions are made. Thank you. [[ We apologize if you receive this more than once ]] The 2022 ACL2 Workshop will be held (tentatively) in Austin and (certainly) online. We invite ACL2 users, experts and beginners alike, users of other theorem provers, and persons interested in the applications of theorem proving technology to submit papers to the Workshop. * Important Dates Abstract Submission: February 22, 2022 Paper Submission: March 1, 2022 Author Notification: April 5, 2022 Camera-Ready Copy: April 26, 2022 Workshop: May 26-27, 2022 * Website More information may be found at: https://www.cs.utexas.edu/users/moore/acl2/workshop-2022/index.html * 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-2022 is a two-day workshop to be held in Austin and online on May 26-27, 2022. It is the 17th in the series of ACL2 workshops, which occur approximately every 18 months. The workshop will feature invited speakers, technical papers, and rump sessions that discuss ongoing research. We invite submissions of papers on any topic related to ACL2 and its applications. We strongly encourage submissions from new members of the ACL2 community, including graduate students and researchers who are primarily involved with other theorem provers or formal methods. 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. and they should be prepared in the EPTCS templates, available from http://style.eptcs.org. All papers must be submitted via EasyChair at https://easychair.org/my/conference?conf=acl22022. 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 require short abstracts to be submitted by the "Abstract submission" deadline and will be refereed by at least three members of the program committee. 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 interested readers can pursue the abstract topic. Regular papers and extended abstracts must describe work that has already been done, not simply ideas for future work. Current and planned (or suggested) work may be presented in the Rump Sessions. 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). Regular papers will be published as PDFs, and extended abstracts will be published as HTML snippets. Please see the EPTCS copyright page (http://copyright.eptcs.org/) for a discussion of licensing. Please also see the EPTCS LaTeX style file and formatting instructions (http://style.eptcs.org). 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: prompt% $ACL2_DIR/books/build/cert.pl --acl2 ACL2 *.lisp Please send the supporting materials to either chair: Rob Sumners (rob.sumners@intel.com, rob.sumners@gmail.com) or Cuong Chau (cuong.chau@arm.com, ckc8687@gmail.com) as a gzipped tarball or whatever format is suitable. The authors can expect the reviewers to take the supporting materials into account during the refereeing process. Authors of accepted papers are required to make these ACL2 books available by adding them to the ACL2 Community Books. (The chairs may assist in that process, if asked.) * Rump Sessions The workshop will also feature "rump sessions," in which participants can describe ongoing or proposed research related to ACL2. Proposals for rump session presentations, including a title and short abstract, may be accepted until the workshop, but preference will be given to early submissions and subject to available time. Rump session proposals should be sent to either chair. * Program Committee Alessandro Coglio, Kestrel Institute Ruben Gamboa, University of Wyoming Shilpi Goel, Intel Corporation Dave Greve, Collins Aerospace David Hardin, Collins Aerospace Warren Hunt, University of Texas at Austin Matt Kaufmann, University of Texas at Austin Panagiotis Manolios, Northeastern University Eric McCarthy, Kestrel Institute Mihir Mehta, Intel Corporation Grant Passmore, Univeristy of Cambridge Yan Peng, University of British Columbia Sandip Ray, University of Florida Jose-Luis Ruiz-Reina, University of Seville David Russinoff, ARM, Inc. Eric Smith, Kestrel Institute Sol Swords, Intel Corporation Mertcan Temel, Intel Corporation * Workshop Co-Chairs Rob Sumners, Intel Corporation Cuong Chau, ARM, Inc. * Steering Committee J Strother Moore, The University of Texas at Austin Matt Kaufmann, The University of Texas at Austin Shilpi Goel, Intel Corporation Ruben Gamboa, University of Wyoming Grant Passmore, University of Cambridge