Advance 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 |