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
16:30-18:00 Session 34Q: Panel Discussion about low-level code verification
Location: FH, Hörsaal 7