VSL 2014: VIENNA SUMMER OF LOGIC 2014
ITP PROGRAM

Days: Monday, July 14th Tuesday, July 15th Wednesday, July 16th Thursday, July 17th

Monday, July 14th, 2014

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

08:45-09:15 Session 37: VSL Opening
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
08:45
Welcome Address by the Rector (abstract)
08:50
Welcome Address by the Organizers (abstract)
08:55
VSL Opening (abstract)
09:15-10:15 Session 38: VSL Keynote Talk
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
09:15
VSL Keynote Talk: Computational Ideas and the Theory of Evolution (abstract)
10:15-10:45Coffee Break
10:45-13:00 Session 38C: Verified Theorem Provers
Location: FH, Hörsaal 8
10:45
Towards a Formally Verified Proof Assistant (abstract)
11:15
The reflective Milawa theorem prover is sound (down to the machine code that runs it) (abstract)
11:45
HOL with Definitions: Semantics, Soundness, and a Verified Implementation (abstract)
12:15
Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (abstract)
12:45
Rough Diamond: An Extension of Equivalence-based Rewriting (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 41B: Invited Talk
Location: FH, Hörsaal 8
14:30
From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle (abstract)
15:00
Invited talk: Microcode Verification - Another Piece of the Microprocessor Verification Puzzle (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 42C: Codatatypes
Location: FH, Hörsaal 8
16:30
Truly Modular (Co)datatypes for Isabelle/HOL (abstract)
17:00
Recursive Functions on Codatatypes via Domains and Topologies (abstract)
17:30
Experience Implementing a Performant Category-Theory Library in Coq (abstract)
Tuesday, July 15th, 2014

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

08:45-10:15 Session 44: FLoC Plenary Talk (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Plenary Talk: From Reachability to Temporal Specifications in Game Theory (abstract)
Monday, July 14th, 2014

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

Tuesday, July 15th, 2014

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

10:15-10:45Coffee Break
10:45-13:00 Session 47C
Location: FH, Hörsaal 8
10:45
A Formal Library for Elliptic Curves in the Coq Proof Assistant (abstract)
11:15
A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (abstract)
11:45
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm (abstract)
12:15
Cardinals in Isabelle/HOL (abstract)
12:45
HOL Constant Definitions Done Right (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 50C: Invited Talk
Location: FH, Hörsaal 8
14:30
Balancing lists: a proof pearl (abstract)
15:00
Invited talk: Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 52B: User Interfaces
Location: FH, Hörsaal 8
16:30
An Isabelle Proof Method Language (abstract)
17:00
Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (abstract)
17:30
Collaborative Interactive Theorem Proving with Clide (abstract)
19:00-20:00 Session 56A: VSL Public Lecture 1
Location: MB, Kuppelsaal
19:00
VSL Public Lecture: Gödel in Vienna (abstract)
Wednesday, July 16th, 2014

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

10:45-13:00 Session 56C: Mathematics
Location: FH, Hörsaal 8
10:45
A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (abstract)
11:15
A Coq Formalization of Finitely Presented Modules (abstract)
11:45
Formal Verification of Optical Quantum Flip Gate (abstract)
12:15
On the Formalization of Z-Transform in HOL (abstract)
12:45
Mechanical Certification of Loop Pipelining Transformations: A Preview (abstract)
08:45-10:15 Session 57: VSL Keynote Talk
Location: EI, EI 7 + EI 9, EI 10 + FH, Hörsaal 1
08:45
VSL Keynote Talk: The theory and applications of o-minimal structures (abstract)
10:15-10:45Coffee Break
13:00-14:30Lunch Break
14:30-16:00 Session 59C: Invited Talk
Location: FH, Hörsaal 8
14:30
Showing invariance compositionally for a process algebra for network protocols (abstract)
15:00
Invited talk: Retrofitting Rigour (abstract)
16:00-16:30Coffee Break
16:30-18:00 Session 61C: Automation
Location: FH, Hörsaal 8
16:30
A heuristic prover for real inequalities (abstract)
17:00
Unified Decision Procedures for Regular Expression Equivalence (abstract)
17:30
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (abstract)
Thursday, July 17th, 2014

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

08:45-10:15 Session 62A: FLoC Panel (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Panel: Publication Models in Computing Research: Is a Change Needed? Are We Ready for a Change? (abstract)
Wednesday, July 16th, 2014

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

Thursday, July 17th, 2014

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

10:15-10:45Coffee Break
10:45-13:00 Session 66AC
Location: FH, Hörsaal 8
10:45
Formalized, effective domain theory in Coq (abstract)
11:15
Completeness and Decidability Results for CTL in Coq (abstract)
11:45
Universe Polymorphism in Coq (abstract)
12:15
Compositional Computational Reflection (abstract)
12:45
Formal C semantics: CompCert and the C standard (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 75AC
Location: FH, Hörsaal 8
14:30
A New and Formalized Proof of Abstract Completion (abstract)
15:00
Hypermap Specification and Certified Linked Implementation using Orbits (abstract)
15:30
Implicational Rewriting Tactics in HOL (abstract)
16:00-16:30Coffee Break
16:30-19:00 Session 79A: VSL Joint Award Ceremony 1
Location: MB, Kuppelsaal
16:30
Foundations and Technology Competitions Award Ceremony (abstract)
17:30
FLoC Olympic Games Award Ceremony 1 (abstract)
18:15
FLoC Closing Week 1 (abstract)
Friday, July 18th, 2014

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

09:00-18:00 Session 87E: FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (joint with 9 other meetings)
Location: FH, 2nd floor
09:00
FLoC Olympic Games Big Screen: Satisfiability Modulo Theories solver competition (SMT-COMP 2014) (abstract)
Thursday, July 17th, 2014

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

Saturday, July 19th, 2014

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

08:45-10:15 Session 106A: FLoC Panel (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Panel: Computational Complexity and Logic: Theory vs. Experiments (abstract)
Sunday, July 20th, 2014

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

08:45-10:15 Session 123: FLoC Plenary Talk (joint with 9 other meetings)
Location: FH, Hörsaal 1
08:45
FLoC Plenary Talk: Electronic voting: how logic can help? (abstract)