Vérification de programmes OCaml fortement impératifs avec Why3

Jean-Christophe Filliâtre 1 Mário Pereira 1 Simão Melo de Sousa 2
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 présente une méthodologie pour prouver des programmes OCaml fortement impératifs avec l'outil de vérification déductive Why3. Pour un programme OCaml donné, un modèle mémoire spécifique est construit et on vérifie un programme Why3 qui le mani-pule. Une fois la preuve terminée, on utilise la capacité de Why3 à traduire ses programmes vers le langage OCaml, tout en remplaçant les opérations sur le modèle mémoire par les opérations correspondantes sur des types mutables d'OCaml. Cette méthode est mise à l'épreuve sur plusieurs exemples manipulant des listes chaînées et des graphes mutables.
Type de document :
Communication dans un congrès
JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. pp.1-14
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-01649989
Contributeur : Mário José Parreira Pereira <>
Soumis le : lundi 11 décembre 2017 - 15:04:43
Dernière modification le : jeudi 11 janvier 2018 - 06:25:27

Fichier

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

Identifiants

  • HAL Id : hal-01649989, version 2

Citation

Jean-Christophe Filliâtre, Mário Pereira, Simão Melo de Sousa. Vérification de programmes OCaml fortement impératifs avec Why3. JFLA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. pp.1-14. 〈hal-01649989v2〉

Partager

Métriques

Consultations de la notice

48

Téléchargements de fichiers

28