Day 1

Day 2

Day 3

Day 4

Day 5

Workshops [download the overall workshops program in pdf]

July 13

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

July 14

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

---

 

 

 

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

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

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

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

 

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

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

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

 

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

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

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

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

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

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

 

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

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

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

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

 

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

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

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

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

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