Skip to Main content Skip to Navigation
Conference papers

Un mécanisme d'extraction vers C pour Why3

Résumé : Nous présentons un mécanisme d'extraction d'un sous-ensemble des programmes écrits avec l'outil de vérification Why3 vers le langage C. Un modèle mémoire partiel mais simple permet aux utilisateurs d'écrire des programmes Why3 dans un style impératif très proche du C, avec une gestion manuelle et vérifiée formellement de la mémoire. De tels programmes peuvent ensuite être extraits de manière transparente vers du code C idiomatique, ce qui évite d'introduire des pertes de performances à l'extraction.
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download

https://hal.inria.fr/hal-01653153
Contributor : Raphaël Rieu-Helft <>
Submitted on : Friday, December 1, 2017 - 10:04:47 AM
Last modification on : Thursday, July 8, 2021 - 3:46:36 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01653153, version 1

Citation

Raphaël Rieu-Helft. Un mécanisme d'extraction vers C pour Why3. 29èmes Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France. ⟨hal-01653153⟩

Share

Metrics

Record views

194

Files downloads

267