Certified algorithms for program slicing

Résumé : La simplification syntaxique, ou slicing, est une technique permettant d’extraire, à partir d’un programme et d’un critère consistant en une ou plusieurs instructions de ce programme, un programme plus simple, appelé slice, ayant le même comportement que le programme initial vis-à-vis de ce critère. Les méthodes d’analyse de code permettent d’établir les propriétés d’un programme. Ces méthodes sont souvent coûteuses, et leur complexité augmente rapidement avec la taille du code. Il serait donc souhaitable d’appliquer ces techniques sur des slices plutôt que sur le programme initial, mais cela nécessite de pouvoir justifier théoriquement l’interprétation des résultats obtenus sur les slices. Cette thèse apporte cette justification pour le cas de la recherche d’erreurs à l’exécution. Dans ce cadre, deux questions se posent. Si une erreur est détectée dans une slice, cela veut-il dire qu’elle se déclenchera aussi dans le programme initial ? Et inversement, si l’absence d’erreurs est prouvée dans une slice, cela veut-il dire que le programme initial en est lui aussi exempt ? Nous modélisons ce problème sur un mini-langage impératif représentatif, autorisant les erreurs et la non-terminaison, et montrons le lien entre la sémantique du programme initial et la sémantique de sa slice, ce qui nous permet de répondre aux deux questions précédentes. Pour généraliser ces résultats, nous nous intéressons à la première brique d’un slicer indépendant du langage : le calcul générique des dépendances de contrôle. Nous formalisons une théorie élégante de dépendances de contrôle sur des graphes orientés finis arbitraires prise dans la littérature et améliorons l’algorithme de calcul proposé.Pour garantir un maximum de confiance dans les résultats, tous ces travaux sont prouvés dans l’assistant de preuve Coq ou dans l’outil de preuve Why3.
Type de document :
Thèse
Autre. Université Paris-Saclay, 2018. Français. 〈NNT : 2018SACLC056〉
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-01874620
Contributeur : Abes Star <>
Soumis le : vendredi 14 septembre 2018 - 14:49:06
Dernière modification le : mardi 2 octobre 2018 - 03:44:39

Fichier

75271_LECHENET_2018_archivage....
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-01874620, version 1

Citation

Jean-Christophe Léchenet. Certified algorithms for program slicing. Autre. Université Paris-Saclay, 2018. Français. 〈NNT : 2018SACLC056〉. 〈tel-01874620〉

Partager

Métriques

Consultations de la notice

168

Téléchargements de fichiers

109