Skip to Main content Skip to Navigation
Conference papers

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

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01649989
Contributor : Mário José Parreira Pereira <>
Submitted on : Monday, December 11, 2017 - 3:04:43 PM
Last modification on : Tuesday, April 21, 2020 - 1:05:34 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

285

Files downloads

524