Advance 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