Wed 20 June  Thu 21 June  Fri 22 June

Wed 20 June

14:30 - 15:00Registration
15:00 - 16:30Tutorial Part I: Software Model Checking for Mobile Security – Collusion Detection in K. Irina Mariuca Asavoae & Markus Roggenbach
16:30 - 17:00Break
17:00 - 18:30Tutorial Part II: Software Model Checking for Mobile Security – Collusion Detection in K. Irina Mariuca Asavoae & Markus Roggenbach
20:30Wellcome Reception

Thu 21 June

09:00 - 09:30Registration
09:30 - 11:00Wellcome & Invited talk: Efficient Runtime Verification of First-Order Temporal Properties. Klaus Havelund & Doron Peled
11:00 - 11:30Break
11:30 - 13:00 Session 1:

- Petri Net Reductions for Counting Markings. Bernard Berthomieu, Didier Le Botlan and Silvano Dal Zilio

- Improving Generalization in Software IC3. Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll and Joost-Pieter Katoen

- Star-Topology Decoupling in SPIN. Daniel Gnad, Patrick Dubbert, Alberto Lluch Lafuente and Joerg Hoffmann
13:00 - 14:30Lunch
14:30 - 15:30Invited talk: Applying Formal methods to Advanced Embedded Controllers. Rémi Delmas
15:30 - 16:00Session 2:

- Joint Forces For Memory Safety Checking. Marek Chalupa, Jan Strejček and Martina Vitovská
16:00 - 16:20Break
16:20 - 18:00Session 3:

- Model-Checking HyperLTL for Pushdown Systems. Adrien Pommellet and Tayssir Touili

- A Branching Time Variant of CaRet. Jens Oliver Gutsfeld, Markus Müller-Olm and Benedikt Nordhoff

- Control strategies for off-line testing of timed systems. Léo Henry, Thierry Jéron and Nicolas Markey

- An extension of TRIANGLE testbed with model-based testing. Laura Panizo, Almudena Díaz and Bruno García
20:30 Social Event

Fri 22 Jul

09:30 - 10:30Invited talk: Program Verification with Separation Logic. Radu Iosif
10:30 - 11:00Session 4:

- Local Data Race Freedom with Non-Multi-Copy Atomicity. Tatsuya Abe
11:00 - 11:30Break
11:30 - 13:00Session 5:

- A Comparative Study of Decision Diagrams for Real-time Model Checking. Omar Bataineh, Mark Reynolds and David Rosenblum

- Lazy Reachability Checking for Timed Automata with Discrete Variables. Tamás Tóth and István Majzik

- From SysML to Model Checkers via Model Transformation. Martin Kölbl, Stefan Leue and Hargurbir Singh
13:00 - 14:30Lunch
14:30 - 15:30Session 6:

- Genetic Synthesis of Concurrent Code using Model Checking and Statistical Model Checking. Lei Bu, Doron Peled, Dachuan Shen and Yuan Zhuang

- Quantitative Model Checking for a Controller Design. Youngmin Kwon and Eunhee Kim
15:30 - 16:00Break
16:00 - 17:00Session 7:

- Modelling Without a Modelling Language. Antti Valmari and Vesa Lappalainen

- Context-Updates Analysis and Refinement in Chisel. Irina Mariuca Asavoae, Mihail Asavoae and Adrian Riesco
17:00 - 17:30Best paper award & Closing