Day 1 Day 2 Day 3 Day 4 Day 5

Workshops [download the overall workshops program in pdf]

July 13

(EC)2 (room Foxtrott 2), FWFM (room Jazz), Interpolation (room Foxtrott 1), SYNT (room Foxtrott 3), VES (room Soul), VPT (room Blues)

July 14

(EC)2 (room Foxtrott 2), Interpolation (room Foxtrott 1), REORDER (room Soul)VeriSure (room Jazz)SYNT (room Foxtrott 3), VPT (room Blues)




Day 1 (July 15)

9:00-10:30 Tutorial 1

Chair: Bernd Finkbeiner
Cristian Cadar (Imperial College London): Dynamic Symbolic Execution

10:30 Coffee

11:00-12:30 Tutorial 2

Chair: Arie Gurfinkel
Andreas Podelski (University of Freiburg): Software Model Checking for People who Love Automata

12:30 Lunch

13:30-15:00 Tutorial 3

Chair: Nikolaj Bjoerner
Andrei Voronkov (The University of Manchester): First-Order Theorem Proving and Vampire

15:00 Coffee

15:30-17:00 Tutorial 4

Chair: Roderick Bloem
David Harel (The Weizmann Institute of Science): Can we Computerize an Elephant? On the Grand Challenge of Modeling a Complete Multi-Cellular Organism

17:40 Leaving the hotel to the Neva embankment

18:00 Boarding the excursion boats

18:30-20:30 Boat Tour in Canals of St. Petersburg (incl. Reception) (see the route)


Day 2 (July 16)

9:00-10:30 Session 1: Hybrid Systems

Chair: Javier Esparza

09:00  Hui Kong, Fei He, Xiaoyu Song, William Hung and Ming Gu: Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems

09:20  Alexandre Donzé, Thomas Ferrere and Oded Maler: Efficient Robust Monitoring for STL

09:40  Pavithra Prabhakar and Miriam Garcia Soto: Abstraction based Model-Checking of Stability of Hybrid Systems

10:00  Toni Mancini, Federico Mari, Annalisa Massini, Igor Melatti, Fabio Merli and Enrico Tronci: System Level Formal Verification via Model Checking Driven Simulation

10:20  Xin Chen, Erika Abraham and Sriram Sankaranarayanan: Flow*: An Analyzer for Non-Linear Hybrid Systems

10:30 Coffee

11:00-12:00 Session 2: Invited Talk

 Chair: Helmut Veith
Jennifer Welch (Texas A&M University): Challenges for Formal Methods in Distributed Computing

12:00 Lunch

13:30-15:20 Session 3: Software Verification

Chair: Domagoj Babic

13:30  William Harris, Guoliang Jin, Shan Lu and Somesh Jha: Validating Library Usage Interactively

13:50  Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider: Learning Universally Quantified Invariants of Linear Data Structures

14:10  Maximilien Colange, Souheib Baarir, Fabrice Kordon and Yann Thierry-Mieg: Towards Software Model Checking using Data Decision Diagrams

14:30  Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki and Edmund Clarke: Automatic Abstraction in SMT-Based Unbounded Software Model Checking

14:50  Tewodros Beyene, Corneliu Popeea and Andrey Rybalchenko: Solving Existentially Quantified Horn Clauses

15:10  Jiri Barnat, Lubos Brim, Vojtěch Havel, Jan Havlíček, Jan Kriho, Milan Lenco, Petr Ročkai, Vladimír Štill and Jiří Weiser: DiVinE 3.0 — Explicit-state Model-checker for Multithreaded C/C++ Programs

15:20 Coffee

16:00-17:30 Panel: Future of CAV

19:00-22:00 PC Dinner


Day 3 (July 17)

9:00-10:20 Session 4: Interpolation

Chair: Georg Weissenbacher

09:00  Aws Albarghouthi and Ken McMillan: Beautiful Interpolants

09:20  Yakir Vizel, Vadim Ryvchin and Alexander Nadel: Efficient Generation of Small Interpolants in CNF

09:40  Philipp Ruemmer, Hossein Hojjat and Viktor Kuncak: Disjunctive Interpolants for Horn-Clause Verification

10:00  Liyun Dai, Bican Xia and Naijun Zhan: Generating Non-Linear Interpolants by Semidefinite Programming

10:20 Coffee

10:50-12:00 Session 5: Biology

Chair: Marta Kwiatkowska

10:50  Loïc Paulevé, Geoffroy Andrieux and Heinz Koeppl: Under-approximating Cut Sets for Reachability in Large Scale Automata Networks

11:10  Koen Claessen, Jasmin Fisher, Samin Ishtiaq, Nir Piterman and Qinsi Wang: Model-Checking Signal Transduction Networks through Decreasing Reachability Sets

11:30  Lubos Brim, Milan Ceska, Sven Drazan and David Šafránek: Exploring Parameter Space of Stochastic Biochemical Systems using Quantitative Model Checking

11:50  Johannes G. Reiter, Ivana Bozic, Krishnendu Chatterjee and Martin A. Nowak: TTP: Tool for Tumor Progression

12:00 Lunch

13:30-14:30 Session 6: Hardware

Chair: William Hung

13:30  Roy Armoni, Dana Fisman and Naiyong Jin: SVA and PSL Local Variables – A Practical Approach

13:50  Thomas Braibant and Adam Chlipala: Formal Verification of Hardware Synthesis

14:10  Guanfeng Lv, Kaile Su and Yanyan Xu: CacBDD: A BDD Package with Dynamic Cache Management

14:20  Brad Bingham, Jesse Bingham, John Erickson and Mark Greenstreet: Distributed Explicit State Model Checking of Deadlock Freedom

14:30-15:40 Session 7: Shape Analysis

Chair: Florian Zuleger

14:30  Lukas Holik, Ondrej Lengal, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar: Fully Automated Shape Analysis Based on Forest Automata

14:50  Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleks Nanevski and Mooly Sagiv: Effectively Propositional Reasoning about Reachability in Linked Data Structures

15:10  Ruzica Piskac, Thomas Wies and Damien Zufferey: Automating Separation Logic using SMT

15:30  Christoph Haase, Samin Ishtiaq, Joel Ouaknine and Matthew Parkinson: SeLoger: A Tool for Graph-Based Reasoning in Separation Logic

15:40 Coffee

16:10-16:50 Session 8: Invited talk

Chair: Bob Kurshan
Maria Vozhegova (Sberbank): Information Technology in Russia

17:00-18:10 Session 9: SAT and SMT I

Chair: Ofer Strichman

17:00  Joao Marques-Silva, Mikolas Janota and Anton Belov: Minimal Sets over Monotone Predicates in Boolean Formulae

17:20  Supratik Chakraborty, Kuldeep S. Meel and Moshe Vardi: A Scalable and Nearly Uniform Generator of SAT Witnesses

17:40  Loris D’Antoni and Margus Veanes: Equivalence of Extended Symbolic Finite Transducers

18:00  Chih-Hong Cheng, Harald Ruess and Natarajan Shankar: JBernstein: A Validity Checker for Generalized Polynomial Constraints

18:30 Leaving the hotel to the restaurant

19:00-23:30: Banquet (pereulok Tamozhenniy 2)


Day 4 (July 18)

9:00-10:20 Session 10: New domains

Chair: Somesh Jha

09:00  Oshri Adler, Cindy Eisner and Tatyana Veksler: Relative Equivalence in the Presence of Ambiguity

09:20  Arun Chaganty, Akash Lal, Aditya Nori and Sriram Rajamani: Combining Relational Learning with SMT Solvers using CEGAR

09:40  Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus: A Fully Verified Executable LTL Model Checker

10:00  Shaull Almagor, Guy Avni and Orna Kupferman: Automatic Generation of Quality Specifications

10:20 Coffee

10:50-12:00 Session 11: SAT and SMT II

Chair: Laura Kovacs

10:50  Andrew Reynolds, Cesare Tinelli, Amit Goel and Sava Krstic: Finite Model Finding in SMT

11:10  Panagiotis Manolios and Vasilis Papavasileiou: ILP Modulo Theories

11:30  Richard Uhler and Nirav Dave: Seri: Automatic Translation of High-level Symbolic Computations into SMT Queries

11:50  Isil Dillig and Thomas Dillig: EXPLAIN: A Tool for Performing Abductive Inference

12:00 Lunch

13:30-15:20 Session 12: Synthesis

Chair: Ruzica Piskac

13:30  Christian Von Essen and Barbara Jobstmann: Program Repair without Regret

13:50  Daniel Wonisch, Alexander Schremmer and Heike Wehrheim: Programs from Proofs – A PCC Alternative

14:10  Aws Albarghouthi, Sumit Gulwani and Zachary Kincaid: Recursive Program Synthesis

14:30  Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach: Efficient synthesis for concurrency using semantics-preserving transformations

14:50  Ming-Hsien Tsai, Yih-Kuen Tsay and Yu-Shiang Hwang: GOAL for Games, Omega-Automata, and Logics

15:00  Romain Brenguier: PRALINE: A Tool for Computing Nash Equilibria in Concurrent Games

15:10  Ayrat Khalimov, Swen Jacobs and Roderick Bloem: PARTY: Parameterized Synthesis of Token Rings

15:20 Coffee

16:00-17:00 Session 13: Time

Chair: Josef Widder

16:00  Alfons Laarman, Mads Chr. Olesen, Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen and Jaco Van De Pol: Multi-Core Emptiness Checking of Timed Buchi Automata using Inclusion Abstraction

16:20  Frédéric Herbreteau, B Srivathsan and Igor Walukiewicz: Lazy abstractions for timed automata

16:40  Étienne André, Yang Liu, Jun Sun, Jin Song Dong and Shang-Wei Lin: PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems

16:50  Ocan Sankur: Shrinktech: A Tool for the Robustness Analysis of Timed Automata

17:00-18:30 Session 14: Tool demos and posters

18:30-19:30 Business Meeting

19:30-21:30 SC Dinner


Day 5 (July 19)

9:00-10:40 Session 15: Concurrency

Chair: Azadeh Farzan

09:00  Pierre Ganty, Javier Esparza and Rupak Majumdar: Parameterized Verification of Asynchronous Shared-Memory Systems

09:20  Jade Alglave, Daniel Kroening and Michael Tautschnig: Partial Orders for Efficient BMC of Concurrent Software

09:40  Johannes Kloos, Rupak Majumdar, Filip Niksic and Ruzica Piskac: Incremental, Inductive Coverability

10:00  Cezara Dragoi, Ashutosh Gupta and Thomas Henzinger: Automatic linearizability proofs of concurrent objects with cooperating updates

10:20  Azadeh Farzan and Zachary Kincaid: Duet: Static Analysis for Unbounded Parallelism

10:30 Coffee

11:10-12:10 Session 16: Invited Talk

Chair: Natasha Sharygina
Jeannette Wing (Microsoft Research International): Formal Methods from an Industrial Perspective

12:10 Lunch

13:30-15:30 Session 17: Probabilistic and Statistical

Chair: Marta Kwiatkowska

13:30  Alistair Stewart, Kousha Etessami and Mihalis Yannakakis: Upper bounds for Newton’s method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata

13:50  Aleksandar Chakarov and Sriram Sankaranarayanan: Probabilistic Program Analysis with Martingales

14:10  Alberto Puggelli, Wenchao Li, Alberto Sangiovanni-Vincentelli and Sanjit Seshia: Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties

14:30  Krishnendu Chatterjee and Jakub Łącki: Faster Algorithms for Markov Decision Processes with Low Treewidth

14:50  Krishnendu Chatterjee, Andreas Gaiser and Jan Kretinsky: Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

15:10  Cyrille Jegourel, Axel Legay and Sean Sedwards: Importance Splitting for Statistical Model Checking Rare Properties

15:30 Coffee

16:00-17:10 Session 18: Security

Chair: Daniel Kroening

16:00  Vincent Cheval, Veronique Cortier and Antoine Plet: Lengths may break privacy — or how to check for equivalences with length

16:20  Adi Sosnovich, Orna Grumberg and Gabi Nakibly: Finding Security Vulnerabilities in a Network Protocol using Parameterized Systems

16:40  Tom Chothia, Yusuke Kawamoto and Chris Novakovic: A Tool for Estimating Information Leakage

16:50  Simon Meier, Benedikt Schmidt, Cas Cremers and David Basin: The TAMARIN Prover for the Symbolic Analysis of Security Protocols

17:00  Fabrizio Biondi, Andrzej Wasowski, Axel Legay and Louis-Marie Traonouez: QUAIL: a quantitative security analyzer for imperative code

17:10-18:10 Session 19: Loops and Termination

Chair: Florian Zuleger

17:10  Daniel Kroening, Matt Lewis and Georg Weissenbacher: Under-Approximating Loops in C Programs for Fast Counterexample Detection

17:30  Pierre Ganty and Samir Genaim: Proving Termination Starting from the End

17:50  Marc Brockschmidt, Byron Cook and Carsten Fuhs: Better termination proving through cooperation

19:00-21:30 Informal party