Model Checking Reading Club/Suggestions for Papers (2010-2011)

---

• David Jansen:

- 'A counterexample is no longer a single run as in CTL model checking, but a set of runs' by Han and Katoen.

- 'Robust timed automata. If clocks in a timed automaton may drift a little, which TCTL properties do still hold?' by Dima

• Freek Verbeek:

- 'D-Finder: A Tool for Compositional Deadlock Detection and Verification' by Bensalem

- Bounds on evacuation time for deflection routing' by Hajek

- SAT/SMT solver

• Faranak Heidarian:

- 'MCMT in the Land of Parameterized Timed Automata' by Carioni, Ghilsrdi,and Ranise - 'Goal-directed Invariant Synthesis for Model Checking Modulo Theories' by Ghilsrdi and Ranise

• Martijn Hendriks:

- Design Space Exploration, multiobjective optimization

• Georgeta Igna:

- Robust Timed Automata - Partial Order Reduction

• Fides Aarts:

- Nondeterministic Systems - Optimal strategies for testing nondeterministic systems by Nachmanson, Veanes, Schulte, Tillmann, and Grieskamp

• Frits Vaandrager:

- The Daikon system for dynamic detection of likely invariants by Ernst, Perkins, Guo, McCamant, Pacheco, Tschantz,and Xiao

N.B: The idea is that we are going to have more rounds of presentations. In each round, every person mentioned above presents one paper proposed.

---