Thematic team Pole Automata, structures and verification Modeling and verification Head Eugène Asarin 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. Seminar Verification seminar Permanent members Name@PhoneOfficePositionPoleTeam Asarin Eugène @ 01 57 27 92 34 4040 Professor ASV verif Bernardi Giovanni @ 01 57 27 93 38 4021 Associate Professor ASV , PPS verif , systemes , preuves Bouajjani Ahmed @ 01 57 27 92 64 4023 Professor ASV verif Degorre Aldric @ 01 57 27 92 32 4018 Associate Professor ASV verif Foughali Mohammed @ 01 57 27 94 49 4043 Associate Professor ASV verif Guessarian Irène @ 01 57 27 92 59 3032 Professor Emeritus - Sorbonne Université 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 Jurski Yan @ 01 57 27 94 41 4027 Associate Professor ASV verif Laroussinie François @ 01 57 27 92 42 4034 Professor ASV verif Sangnier Arnaud @ 01 57 27 92 58 3022 Associate Professor ASV verif Schmitz Sylvain @ 01 57 27 92 16 3048 Professor ASV automates , verif Shirmohammadi Mahsa @ 01 57 27 92 29 4017 Research Scientist - CNRS ASV verif Treinen Ralf @ 01 57 27 92 44 3021 Professor PPS , ASV systemes , verif Non-permanent members Name@PhoneOfficePositionPoleTeam Allombert-Goget Adam @ Intern ASV verif Bigeon Emmanuel @ 3018 Teaching and Research Assistant ASV verif Boutglay Wael-Amine @ 4059 PhD Student ASV verif Chouai Salim @ Visitor ASV verif Cirisci Berk @ 01 57 27 94 56 4033 PhD Student ASV verif Gros Basile @ Intern ASV , PPS verif , systemes , preuves Guillou Lucie @ 4059 PhD Student ASV verif Jacobo-Inclan Bernardo @ PhD Student ASV verif Nagendra Srinidhi @ 4060 PhD Student ASV verif Nehai Zeinab @ 4059 PhD Student ASV , ASD verif , distribue Nosan Klara @ 4031 PhD Student ASV verif Rino Neha @ Intern ASV verif Rolland Julien @ 4053 PhD Student ASV verif Roman-Calvo Enrique @ 4060 PhD Student ASV verif Stietel Olivier @ 3035 PhD Student ASV verif