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

8:00-9:00

Registration & Breakfast

9:00-9:15

Welcome

Session 1

9:15-9:45

Abstract Stobjs and Their Application to ISA Modeling

Shilpi Goel, Warren A Hunt, Jr. and Matt Kaufmann

9:45-10:15

A Step-Indexing Approach to Partial Functions

David Greve and Konrad Slind

Rump Session

10:30-10:45

SAT Proof Checking

Warren Hunt

10:45-11:00

Model Validation

Warren Hunt

11:00-11:15

Code Walker Tool

J Moore

11:15-11:30

Tau and Bounders

J Moore

11:30-11:45

Convergence and Divergence of Infinite Series in ACL2(r)

John Cowles & Ruben Gamboa

11:45-12:00

Termination of Tarai Functions

Tom Bailey, John Cowles & Ruben Gamboa

Lunch

12:00-1:30

Lunch Provided

Session 2

1:30-2:00

Verified AIG Algorithms in ACL2

Jared Davis and Sol Swords

2:00-2:30

A formalisation of XMAS

Bernard van Gastel and Julien Schmaltz

2:30-3:00

A Macro for Reusing Abstract Functions and Theorems

Sebastiaan J. C. Joosten, Bernard van Gastel and Julien Schmaltz

Panel 1

3:30-4:30

ACL2 Book Repository

David Rager & Others To Be Announced

Business Meeting 1

4:30-5:00

Business Meeting

Matt Kaufmann and J Strother Moore

Reception

6:00-8:00

Welcome Reception

Friday, May 31

8:00-9:00

Breakfast

Session 3

9:00-9:30

An Interpreter for Quantum Circuits

Lucas Helms and Ruben Gamboa

9:30-10:00

ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2

David S. Hardin and Samuel S. Hardin

10:00-10:30

Verification of Building Blocks for Asynchronous Circuits

Freek Verbeek and Julien Schmaltz

Panel 2

11:00-12:00

Using ACL2 to Teach Undergraduates

Pete Manolios, J Moore, Warren Hunt, Ruben Gamboa & Sudarshan Srinivasan

Lunch

12:00-1:30

Lunch Provided

Panel 3

1:30-2:00

ACL2 Extension Fragmentation

Matt Kaufmann, Ruben Gamboa, Pete Manolios, Jared Davis, David Rager

Session 4

2:30-3:00

Proof Pad: A New Development Environment for ACL2

Caleb Eggensperger

3:00-3:30

Embedding ACL2 Models in End-User Applications

Jared Davis

Session 5

4:00-4:30

Enhancements to ACL2 in Versions 5.0, 6.0, and 6.1

Matt Kaufmann and J Strother Moore

4:30-5:00

Business Meeting

Matt Kaufmann and J Strother Moore

Banquet

7:00-9:00

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