Deductive Verification via Ghost Debugging

Martin Clochard 1, 2 Andrei Paskevich 1 Claude Marché 1
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Nous présentons une nouvelle approche de vérification de programmes que nous appelons Débogage Fantôme. Cette approche apporte des gains notables lorsque la structure syntaxique du code source du programme à vérifier ne correspond pas à la structure de son exécution, notamment lorsque cette dernière est récursive. Nous présentons un fondement théorique de notre approche sur une variante de jeux transfinis, qui nous permet de spécifier et prouver des propriétés fines sur les comportements infinis des programmes. En utilisant la structure du jeu, nous montrons également que notre approche peut être appliquée à des propriétés relationnelles comme la simulation entre les programmes. Notre approche est formalisée par un développement dans l’outil Why3, qui nous permet de valider mécaniquement la correction de la logique à la Hoare qui sous-tend notre approche.
Type de document :
Rapport
[Research Report] RR-9219, Inria Saclay Ile de France. 2018
Liste complète des métadonnées

https://hal.inria.fr/hal-01907894
Contributeur : Claude Marché <>
Soumis le : lundi 29 octobre 2018 - 15:57:43
Dernière modification le : mardi 5 mars 2019 - 09:30:11
Document(s) archivé(s) le : mercredi 30 janvier 2019 - 16:46:21

Fichier

RR-9219.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01907894, version 1

Citation

Martin Clochard, Andrei Paskevich, Claude Marché. Deductive Verification via Ghost Debugging. [Research Report] RR-9219, Inria Saclay Ile de France. 2018. 〈hal-01907894〉

Partager

Métriques

Consultations de la notice

56

Téléchargements de fichiers

44