Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

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-Sud

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.