Program ACL2 workshop (Vienna, 2014)

Vienna Summer of Logic
Location: FH, Hörsaal 7
The proceedings are online at (click here)

Saturday, July 12th
Sunday, July 13th

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)

(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)
(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)
(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

Ludwig and Adele
Akademiestraße 13
1010 Wien