Leader


Research themes

The research activities of the Modeling and Verification team address the development of algorithmic approaches to system verification, from theoretical foundations to innovative verification tools.

The applications are in a wide spectrum including distributed algorithms, dynamic networks of communicating processes, real-time systems, safety critical embedded systems, programs with complex data structures, concurrent programs, etc.

The adopted approaches are in general based on the use of (1) formal models describing the behaviors of the systems at some abstraction level, (2) formal specifications describing the properties that these systems should satisfy, and (3) algorithmic methods for either establishing the correctness, or detecting illegal behaviors, of a system with respect to its specification.

The models and specification formalisms are in general either automata-based (finite-state automata, pushdown automata, timed or counter automata, etc.) or logic-based (temporal logics, monadic first/second order logics, fixpoint calculi, etc.), and verification problems are often reduced to decision problems for these formalisms such as reachability/language emptiness for the automata, satisfiability/validity for the logics, winning strategies for games, etc. The main issues concern the decidability and the complexity of these problems, as well as the development of efficient verification techniques based on (upper/lower) refinable approximate analysis.

The team has competences in infinite-state verification, verification/synthesis of timed and hybrids systems, temporal logics, games and model-checking, quantitative model-checking, program verification.


Members

NamePhoneOfficePositionMail
Asarin Eugène 01 57 27 92 34 4040 Professeur.e Mail
Bernardi Giovanni 01 57 27 93 38 4026 Maître.sse de conférence Mail
Biswas Ranadeep Doctorant.e Mail
Bouajjani Ahmed 01 57 27 92 64 4023 Professeur.e Mail
Bouillaguet Quentin Doctorant.e Mail
Cauderlier Raphael 4058 Post-Doctorant.e Mail
Degorre Aldric 01 57 27 92 32 4018 Maître.sse de conférence Mail
Delbianco German-Andres 01 57 27 94 07 4032 Post-Doctorant.e Mail
Enea Constantin 01 57 27 92 41 4028a Maître.sse de conférence Mail
Fang Bin 4061 Doctorant.e Mail
Guessarian Irène 01 57 27 92 59 4049 Professeur.e émérite Mail
Habermehl Peter 01 57 27 92 58 3022 Maître.sse de conférence Mail
Horn Florian 01 57 27 94 46 4039 Chargé.e de recherche Mail
Jeannerod Nicolas 01 57 27 92 22 3035 Doctorant.e avec mission d'enseignement Mail
Laroussinie François 01 57 27 92 42 4004 Professeur.e Mail
Long Teng 3007 Maître.sse de conférence Mail
Petri Gustavo 01 57 27 94 01 4021 Maître.sse de conférence Mail
Pommellet Adrien 01 57 27 92 27 4052 ATER Mail
Sangnier Arnaud 01 57 27 92 58 3022 Maître.sse de conférence Mail
Sighireanu Mihaela 01 57 27 94 01 4021 Maître.sse de conférence Mail
Treinen Ralf 01 57 27 92 44 3021 Professeur.e Mail
Wang Chao Post-Doctorant.e Mail