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
|