Ecole Polytechnique Fédérale de Lausanne
Model Checking 2007
english only

Model Checking 2007: Miniprojects

  Topic Type Supervisor Student
1 SAT-based model checking in Mocha Implementation    Aaron Bradley Polina Makeeva
2 PCTL and probabilistic model checking Theory Maria Mateescu Razvan Giuclea
3 Assumptions on non-winning games Theory Barbara Jobstmann   Tatjana Petrov
4 A Mocha to Vis translator Implementation Barbara Jobstmann Sebastian Gfeller
5 Markov Chain trace-equivalence Implementation Laurent Doyen Thibaud Hottelier
6 Survey on minimizing Markov Chains Theory Laurent Doyen Alexandru Arion
7 Extension to Blast Implementation Gregory Theoduloz Damien Zufferey
8 TM data structure algorithm Implementation Vasu Singh Olivier Gobet
9 Multisets Theory Viktor Kuncak Ruzica Piskac
10 Formal Methods for Automated Invariant Generation Theory Laura Kovacs Quentin Heath
11 Distinguishing power of STL without ∃Ο Theory Tom Henzinger -
12 Cost of finding optimal symmetry reduction Theory Tom Henzinger Philippe Suter
13 Automatic Specification Generation Theory/Implementation Viktor Kuncak Masoud Alipour