Vérification formelle des systèmes complexes
Mardi 10 février 2026 à 10h30
ENS Paris-Saclay, Salle 1B26, and online
Résumé : La vérification des systèmes complexes est devenue un enjeu majeur en informatique, car les applications modernes intègrent de plus en plus d'hétérogénéité, d'incertitude et de composants d'apprentissage. Mes recherches abordent ce défi selon trois axes complémentaires : les systèmes partiellement observés, la vérification probabiliste et l'analyse formelle des systèmes d'apprentissage.
Dans un premier temps, j'ai étudié la diagnosticabilité et la prédictibilité en étendant les cadres classiques à des contextes actifs et quantitatifs. J'ai proposé et développé un nouveau cadre d'abstraction-raffinement évolutif (basé sur CEGAR) pour la vérification de la diagnosticabilité des automates temporisés. Son efficacité a été démontrée par des expérimentations sur des jeux de données de référence construits, comblant ainsi le fossé entre complexité théorique et applicabilité pratique. La seconde orientation porte sur les modèles probabilistes, notamment les chaînes de Markov à états infinis, où j'ai étudié le calcul des probabilités d'accessibilité à travers deux propriétés sémantiques: la decisiveness et la divergence. Il convient de noter que la decisiveness a fait l'objet d'une analyse approfondie permettant d'obtenir de nouveaux résultats significatifs, et que la divergence a été introduite et examinée, ces deux éléments ouvrant la voie à des algorithmes génériques pour calculer l’approximation de l'accessibilité. Enfin, je me suis également intéressé à l'exploration de la vérification formelle des systèmes d'apprentissage, en abordant à la fois l'amélioration des performances de la vérification des réseaux de neurones et l'analyse de la robustesse des algorithmes d'apprentissage.
Ensemble, ces contributions visent à établir un cadre unifié pour la vérification formelle et fiable des systèmes dynamiques, stochastiques et d'apprentissage.
Jury :
- Benoît Delahaye, Professeur des Universités, Nantes Université - LS2N (Rapporteur)
- Eric Fabre, Directeur de recherche, Centre Inria de l'Université de Rennes (Rapporteur)
- Louise Travé-Massuyès, Directrice de recherche, LAAS-CNRS (Rapporteuse)
- Béatrice Bérard, Professeur émérite, Sorbonne Université., LIP6 - CNRS (Examinatrice)
- Nathalie Bertrand, Directrice de recherche, Centre Inria de l'Université de Rennes et IRISA (Examinatrice)
- Julien Signoles, Directeur de recherche, Université Paris-Saclay, CEA, List (Examinateur)