Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Extensions de l’algorithme d’atteignabilité arrière dans le cadre de la vérification de modèles modulo théories
Début le 01/10/2015
Direction : CONCHON, Sylvain
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI - salle 465 du PCRI, bâtiment 650 Ada Lovelace
Soutenue le 19/12/2019 devant le jury composé de :
M. Sylvain CONCHON, Professeur, LRI, Université Paris-Sud, Directeur de thèse
Mme Charlotte TRUCHET, Maîtresse de conférence, LS2N, Université de Nantes, Rapportrice
M. Pascal POIZAT, Professeur, LIP6, Sorbonne Université, Rapporteur
Mme Dominique QUADRI, Professeure, LRI, Université Paris-Sud, Examinatrice
M. Philippe QUÉINNEC, Professeur, IRIT, ENSEEIHT, Examinateur
M. Étienne ANDRÉ, Professeur, LORIA, Université de Lorraine, Examinateur
Activités de recherche :
Résumé :
Cette thèse se propose de présenter plusieurs extensions ayant été ajoutées au vérificateur de modèles Cubicle.
Cubicle est un logiciel permettant de vérifier automatiquement la sûreté de systèmes paramétrés au moyen de techniques de vérification de modèles modulo théories.
La première contribution apportée par cette thèse consiste en l'implémentation d'un nouvel algorithme d'atteignabilité baptisé FAR (pour Forward Abstracted Reachabilty). FAR est un algorithme faisant intervenir à la fois des techniques de l'analyse d'atteignabilité en arrière déjà implémentée dans Cubicle ainsi que des techniques d'analyse d'atteignabilité en avant.
La seconde contribution est constituée de multiples ajouts inspirés de méthodes de l'intelligence artificielle afin d'améliorer la génération automatique d'invariants de Cubicle.
Enfin, la dernière contribution a permis d'augmenter l'expressivité de Cubicle afin de prouver des propriétés faisant intervenir des quantificateurs universels. Cette contribution a été mise en œuvre en associant Cubicle à Why3, une plateforme de vérification déductive.
