| Saturday, July 12th |
Sunday, July 13th |
|
| 09:00 |
Welcome |
|
| Morning session (09:15 — 10:15) |
Chair: Freek Verbeek |
Chair: Matt Kaufmann |
| Matt Kaufmann and J Moore. Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4
(slides), (script Holly) |
John Cowles and Ruben Gamboa. Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
(slides)
|
|
| Jared Davis and Matt Kaufmann. Industrial-Strength Documentation for ACL2
(slides) |
Ruben Gamboa and John Cowles. Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
(slides) |
|
| Coffee (10:15 — 10:45) |
||
| Morning session (10:45 — 13:00) |
Chair: Jared Davis |
Chair: Nathan Wetzler |
| Benjamin Selfridge and Eric Smith. Polymorphic Types In ACL2
(slides) |
Benjamin Selfridge. An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
(slides) |
|
| Harsh Raju Chamarthi, Peter Dillinger and Panagiotis Manolios. Data Definitions in ACL2 Sedan
(slides) |
Disha Puri, Sandip Ray, Kecheng Hao and Fei Xie. Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
(slides) |
|
| Jónathan Heras and Ekaterina Komendantskaya. ACL2(ml): Machine-Learning for ACL2
(slides) |
David Russinoff and John O'Leary. Modeling Algorithms in SystemC and ACL2
(slides) |
|
| Sebastiaan Joosten, Cezary Kaliszyk and Josef Urban. Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems
(slides) |
David Hardin, Jennifer Davis, David Greve and Jedidiah McClurg. Development of a Translator from LLVM to ACL2
(slides) |
|
| Lunch (13:00 — 14:30) |
Restaurant Wiener Wirtschaft, Wiedner Hauptstr. 27-29, 1040 Wien |
|
| Afternoon session (14:30 — 16:00) |
Chair: Julien Schmaltz |
Chair: Julien Schmaltz |
| KEYNOTE: Mike Gordon. Linking ACL2 and HOL: past achievements and future prospects
(slides)
|
KEYNOTE:
Magnus Myreen. Machine-code verification: experience of tackling medium-sized case studies using 'decompilation into logic'
(slides) |
|
| RUMP: Ruben Gamboa and John Cowles. Raising (Ir)rationals to (Ir)rational Exponents
(slides)
|
RUMP: Julien Schmaltz. Experiments in high-speed crypto verification |
|
| RUMP: Matt Kaufmann. Browsing the ACL2+Books documentation in Emacs with ACL2-Doc
(emacs commands) |
RUMP: John Erickson. Using testing to automate proofs
(slides)
|
|
| Coffee (16:00 - 16:30) |
||
| Afternoon session (16:30 — 18:00) |
Chair: David Rager |
Chair: Julien Schmaltz |
| RUMP: Ruben Gamboa and John Cowles. On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
(slides)
|
PANEL: low level code verification David Hardin (slides) Warren Hunt Magnus Myreen Anna Slobodova |
|
| RUMP: Nathan Wetzler. Using remove-hyps |
||
| RUMP: Jared Davis. The ACL2 Sidekick | ||
| RUMP: Matt Kaufmann. Desperation Heuristics for ACL2
(slides) |
||
| DISCUSSION: David Rager. Improvements to the books |
||
| Evening session (18:00 -- 19:00) |
Business Meeting |
|
| Diner: Ludwig and Adele Akademiestraße 13 1010 Wien |