Our research in TEMPO focuses the automatic verification of reactive, safety-critical and embedded systems, in which real-time constraints must be taken into account. Those quantitative constraints can be of different natures, and can appear in the models as well as in the properties to be checked.
Permanent Members | ||
| Dietmar Berwanger Researcher, CNRS | Laurent Fribourg Senior researcher, CNRS | Claudine Picaronny Assistant professor, ENS Cachan |
| Patricia Bouyer-Decitre Senior researcher, CNRS | Nicolas Markey Researcher, CNRS | |
Associated and Temporary Members | ||
| Antoine Petit Professor, ENS Cachan
(on leave at INRIA) | ||
Ph.D. Students | ||
| Benoît Barbot PhD student, ENS Cachan | Julien Reichert PhD student, ENS Cachan | Romain Soulat PhD student, ENS Cachan |
| Romain Brenguier PhD student, ENS Cachan | Ocan Sankur PhD student, ENS Cachan | |
| • | . Importance Sampling for Model Checking of Continuous-Time Markov Chains. Research Report LSV-12-08, Laboratoire Spécification et Vérification, ENS Cachan, France, 2012. 15 pages. ( PDF | BibTeX ) |
| • | . Lower-Bound Constrained Runs in Weighted Timed Automata. In QEST'12. IEEE Computer Society Press, 2012. To appear. ( PDF | BibTeX ) |
| • | . Almost-Sure Model-Checking of Reactive Timed Automata. In QEST'12. IEEE Computer Society Press, 2012. To appear. ( BibTeX ) |
| • | . On Termination and Invariance for Faulty Channel Systems. Formal Aspects of Computing, 2012. To appear. ( BibTeX ) |
| • | . Robust Reachability in Timed Automata: A Game-based Approach. In ICALP'12, LNCS. Springer, 2012. To appear. ( PDF | PDF (long version) | BibTeX ) |