VSL 2014: VIENNA SUMMER OF LOGIC 2014
VSTTE PROGRAM

Days: Thursday, July 17th Friday, July 18th

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 66AP: Analysis: Understanding and Explanation
Location: FH, Zeichensaal 3
10:45
Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems (abstract)
11:45
A Model for Capturing and Replaying Proof Strategies (abstract)
12:10
A Verification Condition Visualizer (abstract)
12:35
What Gives? A Hybrid Algorithm for Error Explanation (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 75AN: Verification Frameworks and Applications
Location: FH, Zeichensaal 3
14:30
Efficient Refinement Checking in VCC (abstract)
14:55
Formalizing Semantics with an Automatic Program Verifier (abstract)
15:20
The KeY Platform for Verification and Analysis of Java Programs (abstract)
15:45
Using Promela in a Fully Verified Executable LTL Model Checker (SHORT) (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

08:45-10:15 Session 86F: Hypervisors and dynamic data structures
Location: FH, Zeichensaal 3
08:45
Store Buffer Reduction with MMUs (abstract)
09:10
Separation Kernel Verification: the XtratuM Case Study (abstract)
09:35
Separation algebras for C verification in Coq (abstract)
10:00
Automatically verified implementation of data structures based on AVL trees (SHORT) (abstract)
Thursday, July 17th, 2014

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

Friday, July 18th, 2014

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

10:15-10:45Coffee Break
10:45-13:00 Session 90AM: Certification
Location: FH, Zeichensaal 3
10:45
Up and Out: Scaling Formal Analysis Using Model-Based Development and Architecture Modeling (abstract)
11:45
A logical analysis of framing for specifications with pure method calls (abstract)
12:10
A certifying frontend for (sub)polyhedral abstract domains (abstract)
12:35
Certification of Nontermination Proofs using Strategies and Nonlooping Derivations (abstract)
13:00-14:30Lunch Break
14:30-16:00 Session 96AP: Real Time and Security
Location: FH, Zeichensaal 3
14:30
Model Checking Parameterized Timed Systems (abstract)
14:55
Timed Refinements for Verification of Real-Time Object Code Programs (abstract)
15:20
Formal Modeling and Verification of CloudProxy (abstract)
16:00-16:30Coffee Break