Model Checking Reading Club/Suggestions for Papers (2010-2011)
- '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
- 'D-Finder: A Tool for Compositional Deadlock Detection and Verification' by Bensalem
- Bounds on evacuation time for deflection routing' by Hajek
- SAT/SMT solver
- '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
- Design Space Exploration, multiobjective optimization
- Robust Timed Automata - Partial Order Reduction
- Nondeterministic Systems - Optimal strategies for testing nondeterministic systems by Nachmanson, Veanes, Schulte, Tillmann, and Grieskamp
- 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.
