Défonctionnaliser pour prouver

Mário Pereira 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é : Cet article explore l'idée d'utiliser la défonctionnalisation comme une technique de preuve de programmes. La défonctionnalisation consiste à remplacer les valeurs fonctionnelles par une représentation du premier ordre. L'intérêt est alors de pouvoir utiliser ensuite un outil de preuve de programmes existant, sans lui ajouter de support pour l'ordre supérieur. Cet article illustre et discute cette approche à l'aide de plusieurs exemples et de l'outil de vérification déductive Why3.
Type de document :
Communication dans un congrès
JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01378068
Contributeur : Mário José Parreira Pereira <>
Soumis le : mardi 29 novembre 2016 - 14:01:05
Dernière modification le : jeudi 11 janvier 2018 - 02:01:56
Document(s) archivé(s) le : lundi 27 mars 2017 - 08:43:53

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01378068, version 5

Citation

Mário Pereira. Défonctionnaliser pour prouver. JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. 〈hal-01378068v5〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

43