[TYPES/announce] ACL2 2013 - Call for Participation
Jared C. Davis
jared at cs.utexas.edu
Sat Apr 27 00:17:55 EDT 2013
International Workshop on the ACL2 Theorem Prover
and its Applications
May 30-31, 2013 in Laramie, WY, USA
(Early) Registration Deadline: May 6, 2013
Hotel Deadline: May 15, 2013
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
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.
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
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
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.
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.
Ruben Gamboa, University of Wyoming, USA
Jared Davis, Centaur, USA
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
More information about the Types-announce