| 8:30 - 9:00 | Opening | |
| 9:00 - 10:00 | Invited Talk: Willem Visser (pdf) | |
| 10:00 - 10:30 | Break | |
| 10:30 - 11:00 | Junghee Lim, Akash Lal and Thomas Reps
Symbolic Analysis via Semantic Reinterpretation (pdf) | |
| 11:00 - 11:30 | Andrey Rybalchenko, Rishabh Singh
Subsumer-first: A new Heuristic for Guided Symbolic Reachability Analysis (pdf) | |
| 11:30 - 12:00 | Neha Rungta, Eric Mercer and Willem Visser
Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution (pdf) |
|
| 12:00 - 14:00 | Lunch | |
| 14:00 - 15:00 | Invited Talk: Marta Kwiatkowska (pdf) | |
| 15:00 - 15:30 | Break | |
| 15:30 - 16:00 | Dragan Bosnacki, Stefan Edelkamp, and Damian Sulewski
Efficient Probabilistic Model Checking on General Purpose Graphics Processors (pdf) | |
| 16:00 - 16:30 | Ernst Moritz Hahn, Holger Hermanns and Lijun Zhang
Probabilistic Reachability for Parametric Markov Models (pdf) | |
| 16:30 - 17:00 | Alexander Heussner, Gregoire Sutre and Tristan Le Gall
Extrapolation-based Path Invariants for Abstraction Refinement of Fifo Systems (pdf) |
| 9:00 - 10:00 | Invited Talk: Joseph Sifakis (pdf) | |
| 10:00 - 10.30 | Break | |
| 10:30 - 11:00 | Peter Dillinger and Panagiotis Manolios
Fast, All-Purpose State Storage (pdf) | |
| 11:00 - 11:30 | David Farago and Peter H. Schmitt
Improving Non-progress Cycle Checks (pdf) | |
| 11:30 - 12:00 | Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan and Chao Wang
Automatic Discovery of Transition Symmetry in Multithreaded Programs using Dynamic Analysis (pdf) | |
| 12:00 - 14:00 | Lunch | |
| 14:00 - 14.30 | Nicholas Kidd, Peter Lammich, Tayssir Touili and Thomas Reps
A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks (best) (pdf) | |
| 14:30 - 15:00 | Malay Ganai and Sudipta Kundu
Reduction of Verification Conditions for Concurrent System using Mutually Atomic Transactions (pdf) | |
| 15:00 - 15:30 | Martin Vechev, Eran Yahav and Greta Yorsh
Experience with Checking Linearizability (pdf) | |
| 15:30 - 16:00 | Break | |
| 16:00 - 16:30 | Radek Pelanek and Vaclav Rosecky
EMMA: Explicit Model Checking Manager (pdf) | |
| 16:30 - 17:00 | Tim Kovse, Bostjan Vlaovic, Aleksander Vreze and Zmago Brezocnik
Eclipse Plug-in for Spin and st2msc Tools (pdf) | |
| 17:00 - 17:30 | Mordechai (Moti) Ben-Ari
Teaching Concurrency and Model Checking (pdf) |
| 9:00 - 10:00 | Invited Talk: Patrice Godefroid (pdf) | |
| 10:00 - 10:30 | Break | |
| 10:30 - 11:00 | Damien Thivolle and Hubert Garavel
Verification of GALS Systems by Combining Synchronous Languages and Process Calculi (pdf) | |
| 11:00 - 11:30 | Sebastian Schmerl, Michael Vogel and Hartmut Konig
Identifying Modeling Errors in Signatures by Model Checking (pdf) | |
| 11:30 - 12:00 | Oliver Sharma, Jonathan Lewis, Alice Miller, Al Dearle, Dharini Balasubramaniam, Ron Morrison and Joe Sventek
Towards Verifying Correctness of Wireless Sensor Network Applications using Insense and Spin (pdf) | |
| 12:00 - 12:30 | Closing |