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
Chair:
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
Chair:
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) |
18:00-18:30 Session 43: ITP business meeting
Location: FH, Hörsaal 8
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)
Chair:
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
20:00-21:30 Session 44: VSL Opening Reception
Location: Rathaus
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
Chair:
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)
Chair:
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
19:00-21:30 Session 64: VSL Banquet 1
Location: Schönbrunn
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
Chair:
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 87D: FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (joint with 9 other meetings)
Location: EI, Foyer
| 09:00 | FLoC Olympic Games Big Screen: OWL Reasoner Evaluation (ORE 2014) (abstract) |
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
21:00-23:59 Session 89: VSL Student Reception 1
Location: Transporter
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)
Chair:
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)
Chair:
Location: FH, Hörsaal 1
| 08:45 | FLoC Plenary Talk: Electronic voting: how logic can help? (abstract) |
10:15-18:00 Session 126A: FLoC Olympic Games Big Screen: CASC Automated Theorem Proving System Competition (CASC-J7) (joint with 9 other meetings)
Location: FH, 2nd floor
| 10:15 | FLoC Olympic Games Big Screen: 7th IJCAR ATP System Competition (CASC-J7) (abstract) |
10:15-18:00 Session 126B: FLoC Olympic Games Big Screen: Termination Competition (termComp) (joint with 9 other meetings)
Location: FH, 2nd floor
| 10:15 | FLoC Olympic Games Big Screen: Termination Competition (termCOMP 2014) (abstract) |
14:30-16:00 Session 129G: FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (joint with 9 other meetings)
Location: FH, Hörsaal 2
| 14:30 | FLoC Olympic Games: Answer Set Programming Modeling Competition 2014 (abstract) |