| 9:00 | Welcome Charles Pecheur, Brian Williams |
| 9:15 | Invited Talk:
Large-Scale Parallel Breadth-First Search R. E. Korf and P. Schultze |
| 10:00 | Coffee Break |
| 10:30 | Directed Model Checking Petri Nets Stefan Edelkamp and Shahid Jabbar |
| 11:00 | Relay Reachability Algorithm for Exploring Huge State Space G. Kwon |
| 11:30 | Language-Emptiness Checking of Alternating Tree Automata
Using a Symbolic Reachability Analysis K. Qian A. Nymeyer |
| 12:00 | Dynamic Incremental Hashing in Program Model Checking T. Mehler and S. Edelkamp |
| 12:30 | Lunch Break |
| 2:00 | Incremental Verification for On-the-Fly Controller Synthesis David J. Musliner, Michael J. S. Pelican, Robert P. Goldman |
| 2:30 | Analyzing LTL Model Checking Techniques for Plan Synthesis
and Controller Synthesis S. Kerjean, F. Kabanza, R. St-Denis, and S. Thiebaux |
| 3:00 | Panel/Discussion (topic to be announced) |
| 3:30 | Coffee Break |
| 4:00 | Model Checking Russian Cards Hans van Ditmarsch, Ron van der Meyden, Wiebe van der Hoek, and Ji Ruan |
| 4:30 | Automated Game Analysis via Probabilistic Model Checking: a
case study P. Ballarini, M. Fisher, and M.J. Wooldridge |
| 5:00 | An Approach to Post Mortem Diagnosability Analysis for
Interacting Finite State Systems D. Lawesson, U. Nilsson, and I. Klein |
| 5:30 | Closing Charles Pecheur, Brian Williams |