Email Gateway (Aug 19 2022 at 10:48): Email Gateway (Aug 19 2022 at 10:48):From: "Jared C. Davis" <jared@cs.utexas.edu>
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
Last updated: Nov 21 2024 at 12:39 UTC