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.


Permanent members

Name@PhoneOfficePositionPoleTeam
Asarin Eugène @ 01 57 27 92 34 4040 Professor ASV verif
Bernardi Giovanni @ 01 57 27 93 38 4026 Associate Professor PPS , ASV preuves , systemes , verif
Bouajjani Ahmed @ 01 57 27 92 64 4023 Professor ASV verif
Degorre Aldric @ 01 57 27 92 32 4018 Associate Professor ASV verif
Enea Constantin @ 01 57 27 92 41 4028a Associate Professor ASV verif
Guessarian Irène @ 01 57 27 92 59 4049 Professor Emeritus ASV automates , verif
Habermehl Peter @ 01 57 27 92 58 3022 Associate Professor ASV automates , verif
Horn Florian @ 01 57 27 94 46 4039 Research Scientist - CNRS ASV automates , verif
Laroussinie François @ 01 57 27 92 42 4004 Professor ASV verif
Petri Gustavo @ 01 57 27 94 01 4021 Associate Professor - (en disponibilité) ASV verif
Sangnier Arnaud @ 01 57 27 92 58 3022 Associate Professor ASV verif
Sighireanu Mihaela @ 01 57 27 94 01 4021 Associate Professor ASV verif
Treinen Ralf @ 01 57 27 92 44 3021 Professor PPS , ASV systemes , verif


Non-permanent members

Name@PhoneOfficePositionPoleTeam
Beillahi Sidi-Mohamed @ 4060 PhD Student ASV verif
Biswas Ranadeep @ 01 57 27 94 56 4060 PhD Student ASV verif
Bouillaguet Quentin @ 4021 PhD Student ASV verif
Cauderlier Raphael @ 4058 Post-Doc ASV verif
Delbianco German-Andres @ 01 57 27 94 07 4032 Post-Doc ASV verif
Fang Bin @ 07 68 79 02 80 4061 PhD Student ASV verif
Jeannerod Nicolas @ 01 57 27 92 22 3035 PhD Student with teaching duties PPS , ASV systemes , verif
Ji Kailiang @ 4057 Post-Doc ASV verif
Mutluergil Suha-Orhun @ 01 57 27 94 07 4032 Post-Doc ASV verif
Pommellet Adrien @ 01 57 27 92 27 4052 Teaching and Research Assistant ASV verif
Shirmohammadi Mahsa @ 01 57 27 92 29 4017 Associated Member - CR CNRS ASV verif
Wang Chao @ 01 57 27 94 07 4032 Post-Doc ASV verif
Zennou Rachid @ 0753716448 4058 PhD Student ASV verif