LogoLogo

Giorgino, Mathieu. Inductive representation, proofs and refinement of pointer structures

Giorgino, Mathieu (2013). Inductive representation, proofs and refinement of pointer structures.

[img]
Preview
PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
1964Kb

Résumé en francais

Cette thèse s'intègre dans le domaine général des méthodes formelles qui donnent une sémantique aux programmes pour vérifier formellement des propriétés sur ceux-ci. Sa motivation originale provient d'un besoin de certification des systèmes industriels souvent développés à l'aide de l'Ingénierie Dirigée par les Modèles (IDM) et de langages orientés objets (OO). Pour transformer efficacement des modèles (ou graphes), il est avantageux de les représenter à l'aide de structures de pointeurs, économisant le temps et la mémoire grâce au partage qu'ils permettent. Cependant la vérification de propriétés sur des programmes manipulant des pointeurs est encore complexe. Pour la simplifier, nous proposons de démarrer le développement par une implémentation haut-niveau sous la forme de programmes fonctionnels sur des types de données inductifs facilement vérifiables dans des assistants à la preuve tels que Isabelle/HOL. La représentation des structures de pointeurs est faite à l'aide d'un arbre couvrant contenant des références additionnelles. Ces programmes fonctionnels sont ensuite raffinés si nécessaire vers des programmes impératifs à l'aide de la bibliothèque Imperative_HOL. Ces programmes sont en dernier lieu extraits vers du code Scala (OO). Cette thèse décrit la méthodologie de représentation et de raffinement et fournit des outils pour la manipulation et la preuve de programmes OO dans Isabelle/HOL. L'approche est éprouvée par de nombreux exemples dont notamment l'algorithme de Schorr-Waite et la construction de Diagrammes de Décision Binaires (BDDs).

Sous la direction du :
Directeur de thèse
Matthes, Ralph
Strecker, Martin
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Vérification - Structures de pointeurs - Types de données inductifs - Raffinement - Isabelle/HOL - Graphes - Schorr-Waite - BDDs
Sujets :Informatique
Déposé le :20 Jan 2014 09:29