Programme

Monday, May 12

12:00-14:00 Registration & Lunch

14:00-15:00 Keynote talk: Yannis Smaragdakis (University of Athens): Declarative Static Program Analysis

15:00-16:00 Static Analysis

• Moritz Sinn (Vienna University of Technology): A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis

• Tomer Kotek (Vienna University of Technology): Shape and Content: Incorporating Domain Knowledge into Shape Analysis

16:00-16:30 Coffee break

16:30-18:30 Automated Reasoning

• Ioan Dragan (Vienna University of Technology): Lingva: Generating and Proving Program Properties using Symbol Elimination

• Leonardo Alt (University of Lugano): PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification

• Florian Lonsing (Vienna University of Technology): Incremental QBF Solving

• Klaus Gleissenthall (TUM,Munich): Solving Horn Clauses with Cardinality Constraints

---

Tuesday, May 13

9:00-10:30 Compositional Methods

• Souha Ben Rayana (VERIMAG,Grenoble): Compositional Verification of Component-Based Real-time Systems and Applications

• Corneliu Popeea (TUM,Munich): Reduction for compositional verification of multi-threaded programs

• Najah Bensaid (VERIMAG,Grenoble): Information flow security in component-based systems

10:30-11:00 Coffee break

11:00-12:00 Resources

• Ravichandhran Kandhadai Madhavan (EPFL,Lausanne): Symbolic Resource Bound Inference for Functional Programs

• Ivan Radicek (Vienna University of Technology): Feedback Generation for Performance Problems in Introductory Programming Assignments

12:00-14:00 Lunch break

14:00-15:00 Keynote talk: Dino Distefano (Queen Mary, London and Facebook): Separation Logic Static Analysis @ Facebook

15:00-16:00 Verification I

• Amit Kumar Dhar (LIAFA,Paris): Verification of Properties on Flat Counter Systems

• Frantisek Blahoudek (Masaryk University,Brno): Chasing the Best Buechi Automata for NestedDFS-Based Model Checking

16:00-16:30 Coffee break

16:30-18:00 Distributed Systems

• Alexios Lekidis (VERIMAG,Grenoble): Rigorous modeling and validation of sensor network systems

• Jad Hamza (LIAFA,Paris): Verifying Eventual Consistency of Optimistic Replication Systems

• Benjamin Bittner (FBK,Trento): Failure Propagation Analysis for Safety-Critical Systems

---

Wednesday, May 14

9:00-10:30 Compilation & Synthesis

• Eva Darulova (EPFL,Lausanne): Compiling Real Numbers with Precision Guarantees

• Tewodros Beyene (TUM,Munich): Compositional Repair of Reactive Programs

• Thorsten Tarrach (IST Austria): Regression-free Synthesis for Concurrency

10:30-11:00 Coffee break

11:00-12:00 Verification II

• Marco Gario (FBK,Trento): Using Temporal Epistemic Logic for Reasoning about Fault Management

• Jan Otop and Roopsha Samanta (IST Austria): Robustness Analysis of Transducers

• Lei Song (University of Saarland): An Efficient Model Checking Algorithm of FG-LTL