The list of accepted papers

Programme

Thursday, April 7th
09h00 - 10h00 Room: Blauwe Zaal (Chair: Jean-François Raskin)
ETAPS Unifying Invited Talk: Rupak Majumdar (MPI Kaiserslautern, Germany).
Robots at the Edge of the Cloud
10h00 - 10h30 Coffee Break
10h30 - 12h00 Room: Zwarte Doos
Scheduling and Strategy Synthesis I (Chair: Alice Miller)
  • Maria Del Mar Gallardo, Pedro Merino, Laura Panizo and Alberto Salmerón. River basin management with SPIN
  • Stefan Edelkamp and Christoph Greulich. Using SPIN for the Optimized Scheduling of Discrete Event Systems in Manufacturing
  • Peter Gjøl Jensen, Kim Guldstrand Larsen and Jiri Srba. Real-Time Strategy Synthesis for Timed-Arc Petri Net Games via Discretization
12h30 - 14h00 Lunch
14h00 - 15h00 Room: Zwarte Doos (Chair: Stefan Leue)

Invited Talk: Shaz Qadeer (Microsoft Research, USA).
Programming devices and services in P
15h00 - 15h30 Coffee Break
15h30 - 17h00 Room: Zwarte Doos
Probabilistic Systems (Chair: Pedro Merino)
  • Nishanthan Kamaleson, David Parker and Jonathan Rowe. Finite-Horizon Bisimulation Minimisation for Probabilistic Systems
  • Radu Mateescu and Jose Ignacio Requeno. On-the-Fly Model Checking for Extended Action-Based Probabilistic Operators
  • Ruth Hoffmann, Murray Ireland, Alice Miller, Gethin Norman and Sandor Veres. Autonomous Agent Behaviour Modelled in PRISM -- A Case Study
17h00 - 17h30 Room: Zwarte Doos
Scheduling and Strategy Synthesis II (Chair: Pedro Merino)
  • Ehsan Khamespanah, Kirill Mechitov, Marjan Sirjani and Gul Agha. Schedulability Analysis of Distributed Real-Time Sensor Network Applications using Actor-based Model Checking
18h00 - 23h00 Social event and dinner at the Philips Museum (Emmasingel 31)

Friday, April 8th
09h00 - 10h00 Room: Zwarte Doos (Chair: Dragan Bošnački)

Invited Talk: Pierre Wolper (University of Liège, Belgium).
Model Checking: What Have We Learned, What Will Machines Learn?
10h00 - 10h30 Coffee Break
10h30 - 12h30 Room: Zwarte Doos
Tools (Chair: Radu Mateescu)
  • Kareem Khazem and Michael Tautschnig. smid: A Black-Box Program Driver
  • Jan Mrázek, Petr Bauch, Henrich Lauko and Jiří Barnat. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration
  • Subash Shankar and Gilbert Pajela. A Tool Integrating Model Checking Into a C Verification Toolset
  • Mário Angel Garcia, Felipe Rodrigues Monteiro Sousa, Lucas Carvalho Cordeiro and Eddie de Lima Filho. ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications
12h30 - 14h00 Lunch
14h00 - 15h00 Room: Zwarte Doos (Chair: Anton Wijs)

Invited Talk: Tim Willemse (Eindhoven University of Technology, The Netherlands).
On Verification Challenges at the Large Hadron Collider
15h00 - 16h00 Room: Zwarte Doos
Concurrent System Semantics and Analysis (Chair: Jiří Barnat)
  • Lakhdar Akroun, Gwen Salaün and Lina Ye. Automated Analysis of Asynchronously Communicating Systems
  • Iulia Dragomir, Viorel Preoteasa and Stavros Tripakis. Compositional Semantics and Analysis of Hierarchical Block Diagrams
16h00 - 16h30 Coffee Break
16h30 - 18h00 Room: Zwarte Doos
Model Checking (Chair: Michael Tautschnig)
  • Antti Valmari and Walter Vogler. Fair Testing and Stubborn Sets
  • Aleksandar S. Dimovski. Symbolic Game Semantics for Model Checking Program Families
  • Martin Hofmann, Christian Neukirchen and Harald Ruess. Certification for µ-Calculus with Winning Strategies