[TYPES/announce] ACL2 2013 - Call for Participation

[Jared C. Davis]

                             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

IMPORTANT DATES

          (Early) Registration Deadline:     May  6, 2013
          Hotel Deadline:                    May 15, 2013

WORKSHOP

  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.

  This year's workshop features an exciting collection of
  presentations on a wide variety of topics, such as new modeling
  features and reasoning improvements, new user interfaces, better
  automation for reusing proofs, new approaches to partial functions,
  and applications of ACL2 to verify hardware (including new areas
  such as asynchronous and quantum circuits) and GPU algorithms.

  The workshop will also include panel discussions on the ACL2
  community books and ACL2 version fragmentation.

PRESENTATIONS

  Shilpi Goel, Warren A Hunt, Jr. and Matt Kaufmann.  Abstract Stobjs
  and Their Application to ISA Modeling.

  A David Greve and Konrad Slind.  Step-Indexing Approach to Partial
  Functions.

  Jared Davis and Sol Swords.  Verified AIG Algorithms in ACL2.

  Bernard van Gastel and Julien Schmaltz.  A formalisation of XMAS.

  Sebastiaan J. C. Joosten, Bernard van Gastel and Julien Schmaltz.  A
  Macro for Reusing Abstract Functions and Theorems.

  Lucas Helms and Ruben Gamboa.  An Interpreter for Quantum Circuits.

  David S. Hardin and Samuel S. Hardin.  ACL2 Meets the GPU:
  Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path
  Algorithm in ACL2.

  Freek Verbeek and Julien Schmaltz.  Verification of Building Blocks
  for Asynchronous Circuits.

  Caleb Eggensperger.  Proof Pad: A New Development Environment for
  ACL2.

  Jared Davis.  Embedding ACL2 Models in End-User Applications.

  Matt Kaufmann and J Strother Moore.  Enhancements to ACL2 in
  Versions 5.0, 6.0, and 6.1.

PROCEEDINGS

  Workshop proceedings are freely available electronically as EPTCS
  Volume 114. Printed proceedings will be distributed at the workshop,
  and will also be available for purchase through lulu.com.


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


--
Jared C. Davis <jared at cs.utexas.edu>
11410 Windermere Meadows
Austin, TX 78759
http://www.cs.utexas.edu/users/jared/