Équipe thématique Pôle Automates, structures et vérification Modélisation et vérification Responsable Peter Habermehl Thèmes de recherche Les activités de l'équipe Modélisation et Vérification portent sur le développement d'approches algorithmiques pour la vérification de systèmes, des fondements théoriques aux outils de vérification innovants. Les applications visées sont dans un spectre large comprenant les algorithmes distribués, les réseaux dynamiques de processus communicants, les systèmes temps-réel, les systèmes embarqués critiques, les programmes avec structures de données complexes, les programmes concurrents, etc. Les approches adoptées sont généralement basées sur l'utilisation (1) de modèles formels pour la description à un certain niveau d'abstraction des comportements des systèmes étudiés, (2) de spécifications formelles pour la description des propriétés que doivent satisfaire ces systèmes, et (3) de méthodes algorithmiques soit pour établir la correction, soit pour détecter des comportements illicites, d'un système par rapport à sa spécification. Les modèles et les formalismes de spécification sont de manière générale de type automate (finis, à piles/files, à horloges/compteurs, etc.) ou logique (temporelle, monadique de premier/second ordre, point fixe, etc.), et les problèmes de la vérification sont souvent ramenés à des problèmes de décision sur ces formalismes (accessibilité/langage vide pour les automates, satisfaisabilité pour les logiques, stratégies gagnantes pour les jeux, etc). Se pose alors la question de la décidabilité et de la complexité de ces problèmes, et celle de développer des techniques basées sur le calcul de (sur/sous) approximations raffinables pour résoudre ces problèmes de manière efficace. L'équipe a des compétences dans les domaines de la vérification de systèmes infinis, systèmes temporisés et hybrides, logiques temporelles, jeux et model-checking, model-checking quantitatif, vérification de programmes. Séminaire Séminaire vérification Permanents Nom@TéléphoneBureauFonctionPôleÉquipe Asarin Eugène @ 01 57 27 92 34 4040 Professeur.e ASV verif Bernardi Giovanni @ 01 57 27 94 29 3012 Maître.sse de conférences ASV , PPS verif , preuves , programmes Bouajjani Ahmed @ 01 57 27 92 64 4023 Professeur.e ASV verif Degorre Aldric @ 01 57 27 92 32 4018 Maître.sse de conférences ASV verif Fortin Marie @ 01 57 27 94 00 4016 Chargé.e de recherche - CNRS ASV automates , verif Foughali Mohammed @ 01 57 27 94 49 4043 Maître.sse de conférences ASV verif Guessarian Irène @ 01 57 27 92 59 3032 Professeur.e émérite - Sorbonne Université ASV automates , verif Habermehl Peter @ 01 57 27 92 68 3009 Professeur.e ASV automates , verif Horn Florian @ 01 57 27 94 46 4039 Chargé.e de recherche - CNRS ASV automates , verif Jurski Yan @ 01 57 27 94 41 4027 Maître.sse de conférences ASV verif Laroussinie François @ 01 57 27 92 42 4034 Professeur.e ASV automates , verif Schmitz Sylvain @ 01 57 27 92 16 3048 Professeur.e ASV automates , verif Shirmohammadi Mahsa @ 01 57 27 94 18 4029 Chargé.e de recherche - CNRS ASV verif Touili Tayssir @ 01 57 27 92 61 4028a Directeur.rice de recherche ASV verif Treinen Ralf @ 01 57 27 92 44 3021 Professeur.e PPS , ASV programmes , verif Non-permanents Nom@TéléphoneBureauFonctionPôleÉquipe Amara Mouloud @ Stagiaire ASV verif Boutglay Wael-Amine @ 4059 ATER ASV verif Guillou Lucie @ 4057 Doctorant.e ASV verif Jacobo-Inclan Bernardo @ 3035 Doctorant.e ASV verif Larroque Emile @ 3033 Doctorant.e ASV automates , verif Laversa Laetitia @ 3044 ATER ASV automates , verif Leclercq Loriane @ 3044 ATER ASV verif Lin Shijie @ 3034 Doctorant.e ASV verif Renkin Florian @ 3028 Post-Doctorant.e ASV verif Roman-Calvo Enrique @ 4060 Doctorant.e ASV verif Zhang Maryline @ 4057 Doctorant.e ASV verif Zhangeldinov Olzhas @ 3028 Doctorant.e ASV verif