VSL 2014: VIENNA SUMMER OF LOGIC 2014
ACL2 PROGRAM

Days: Saturday, July 12th Sunday, July 13th

Saturday, July 12th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:15 Session 14: Improvements to ACL2
Location: FH, Hörsaal 7
09:00
Industrial-Strength Documentation for ACL2 (abstract)
09:30
Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (abstract)
10:15-10:45Coffee Break
10:45-13:00 Session 16C: Datatypes and machine learning
Location: FH, Hörsaal 7
10:45
Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (abstract)
11:15
Polymorphic Types In ACL2 (abstract)
11:45
Data Definitions in ACL2 Sedan (abstract)
12:15
ACL2(ml): Machine-Learning for ACL2 (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 18C: Keynote Mike Gordon
Location: FH, Hörsaal 7
14:30
Linking ACL2 and HOL: past achievements and future prospects (abstract)
16:00-16:30Coffee Break
16:30-19:00 Session 20C: Economics, Rump Sessions and Business Meeting
Location: FH, Hörsaal 7
16:30
On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (abstract)
Sunday, July 13th, 2014

View this program: with abstractssession overviewtalk overviewside by side with other conferences

09:00-10:15 Session 23E: Non-standard Analysis
Location: FH, Hörsaal 7
09:00
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent (abstract)
09:30
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (abstract)
10:15-10:45Coffee Break
10:45-13:00 Session 26R: Verification
Location: FH, Hörsaal 7
10:45
Modeling Algorithms in SystemC and ACL2 (abstract)
11:15
Development of a Translator from LLVM to ACL2 (abstract)
11:45
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (abstract)
12:15
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 31N: Keynote Magnus Myreen
Location: FH, Hörsaal 7
14:30
Machine-code verification: experience of tackling medium-sized case studies using 'decompilation into logic’ (abstract)
16:00-16:30Coffee Break