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
CALL FOR PARTICIPATION
May 31-31, 2013 in Laramie, Wyoming
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.
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.
PROGRAM
Thursday, May 30 | |
Welcome | |
|
Registration & Breakfast |
|
Welcome |
Session 1 | |
|
Abstract Stobjs and Their Application to ISA Modeling |
Shilpi Goel, Warren A Hunt, Jr. and Matt Kaufmann | |
|
A Step-Indexing Approach to Partial Functions |
David Greve and Konrad Slind | |
Rump Session | |
|
SAT Proof Checking |
Warren Hunt | |
|
Model Validation |
Warren Hunt | |
|
Code Walker Tool |
J Moore | |
|
Tau and Bounders |
J Moore | |
|
Convergence and Divergence of Infinite Series in ACL2(r) |
John Cowles & Ruben Gamboa | |
|
Termination of Tarai Functions |
Tom Bailey, John Cowles & Ruben Gamboa | |
Lunch | |
|
Lunch Provided |
Session 2 | |
|
Verified AIG Algorithms in ACL2 |
Jared Davis and Sol Swords | |
|
A formalisation of XMAS |
Bernard van Gastel and Julien Schmaltz | |
|
A Macro for Reusing Abstract Functions and Theorems |
Sebastiaan J. C. Joosten, Bernard van Gastel and Julien Schmaltz | |
Panel 1 | |
|
ACL2 Book Repository |
David Rager & Others To Be Announced | |
Business Meeting 1 | |
|
Business Meeting |
Matt Kaufmann and J Strother Moore | |
Reception | |
|
Welcome Reception |
Friday, May 31 | |
|
Breakfast |
Session 3 | |
|
An Interpreter for Quantum Circuits |
Lucas Helms and Ruben Gamboa | |
|
ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2 |
David S. Hardin and Samuel S. Hardin | |
|
Verification of Building Blocks for Asynchronous Circuits |
Freek Verbeek and Julien Schmaltz | |
Panel 2 | |
|
Using ACL2 to Teach Undergraduates |
Pete Manolios, J Moore, Warren Hunt, Ruben Gamboa & Sudarshan Srinivasan | |
Lunch | |
|
Lunch Provided |
Panel 3 | |
|
ACL2 Extension Fragmentation |
Matt Kaufmann, Ruben Gamboa, Pete Manolios, Jared Davis, David Rager | |
Session 4 | |
|
Proof Pad: A New Development Environment for ACL2 |
Caleb Eggensperger | |
|
Embedding ACL2 Models in End-User Applications |
Jared Davis | |
Session 5 | |
|
Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1 |
Matt Kaufmann and J Strother Moore | |
|
Business Meeting |
Matt Kaufmann and J Strother Moore | |
Banquet | |
|
Closing Banquet at Altitude's |
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