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

Inférence d'invariants pour le model checking de systèmes paramétrés

Début le 03/10/2011
Direction : CONCHON, Sylvain
[ZAIDI Fatiha]

Financement :
Etablissement d'inscription : Université Paris-Sud
Lieu de déroulement : LRI PROVAL

Soutenue le 29/09/2014 devant le jury composé de :
Directeur de thèse :
- M. Sylvain Conchon, Professeur, Université Paris-Sud

Co-encadrante :
- Mme Fatiha Zaïdi, Maître de conférences, Université Paris-Sud

Rapporteurs :
- M. Ahmed Bouajjani, Professeur, Université Paris Diderot et IUF
- M. Silvio Ranise, Chercheur, Fondazione Bruno Kessler

Examinateurs :
- M. Rémi Delmas, Ingénieur de recherche, ONERA
- M. Alan Schmitt, Chargé de recherche, INRIA Rennes Bretagne Atlantique
- M. Philippe Dague, Professeur, Université Paris-Sud

Activités de recherche :
   - Démonstration automatique, SMT et applications

Résumé :
Cette thèse aborde le problème de la vérification automatique de systèmes
paramétrés complexes. Cette approche est importante car elle permet de garantir
certaines propriétés sans connaître a priori le nombre de composants du
système. On s'intéresse en particulier à la sûreté de ces systèmes et on traite
le côté paramétré du problème avec des méthodes symboliques. Ces travaux
s'inscrivent dans le cadre théorique du model checking modulo théories et ont
donné lieu à un nouveau model checker : Cubicle.

Une des contributions principale de cette thèse est une nouvelle technique pour
inférer des invariants de manière automatique. Le processus de génération
d'invariants est intégré à l'algorithme de model checking et permet de vérifier
en pratique des systèmes hors de portée des approches symboliques
traditionnelles. Une des applications principales de cet algorithme est
l’analyse de sûreté paramétrée de protocoles de cohérence de cache de taille
industrielle.

Enfin, pour répondre au problème de la confiance placée dans le model checker,
on présente deux techniques de certification de notre outil Cubicle utilisant
la plate-forme Why3. La première consiste à générer des certificats dont la
validité est évaluée de manière indépendante tandis que la seconde est une
approche par vérification déductive du cœur de Cubicle.