Date: Wed, 4 Mar 2015 16:02:23 -0600
Subject: ACL2 2015 - Call For Papers

                     *** CALL FOR PAPERS ***

                              ACL2 2015
        13th International Workshop on the ACL2 Theorem Prover
                         and Its Applications

                October 1-2, 2015, Austin, Texas, USA
                  (immediately following FMCAD 2015)

               Celebrating the 25th anniversary of ACL2

  http://www.cs.utexas.edu/users/moore/acl2/workshop-2015/index.html

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.

IMPORTANT DATES

Abstract submission:   May 26, 2015
Paper submission:      June  2, 2015
Author notification:   July 17, 2015
Camera ready:          August 17, 2015
Workshop:              October 1-2, 2015

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 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, 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

NOTE:

Please see the website

http://www.cs.utexas.edu/users/moore/acl2/workshop-2015/index.html

for further information including paper submission, organization,
venue, lodging, and eventually, registration and program information.