The INFINI axis focuses on verifying infinite systems: programs that manipulate unbounded values, recursive communicating processes, parametrized systems. In this context, our purpose is to identify classes of models and properties for which automated verification is possible.
Permanent Members | ||
| Laurent Doyen Researcher, CNRS | Sylvain Schmitz Assistant professor, ENS Cachan | |
| Alain Finkel Professor, ENS Cachan | Philippe Schnoebelen Senior researcher, CNRS | |
Associated and Temporary Members | ||
| Étienne Lozes Assistant professor, ENS Cachan | Mahsa Shirmohammadi PhD student at ULB | |
Ph.D. Students | ||
| Rémi Bonnet PhD student, ENS Cachan | Julien Reichert PhD student, ENS Cachan | |
| • | . Lexical Disambiguation in LTAG using Left Context. In LTC'11. 2011. ( Web page | BibTeX ) |
| • | . Forward Analysis for WSTS, Part II: Complete WSTS. Logical Methods in Computer Science, 2012. To appear. ( BibTeX ) |
| • | . Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2), pages 97-118, 2011. ( PDF | BibTeX ) |
| • | . Synchronizing Objectives for Markov Decision Processes. In iWIGP'11, Electronic Proceedings in Theoretical Computer Science 50, pages 61-75. 2011. ( PDF | BibTeX ) |
| • | . Games and Markov Decision Processes with Mean-payoff Parity and Energy Parity Objectives. In MEMICS'11, LNCS 7119. Springer, 2011. ( PDF | BibTeX ) |