Un mécanisme d'extraction vers C pour Why3

Raphaël Rieu-Helft 1, 2, 3
3 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 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.
Type de document :
Communication dans un congrès
29èmes Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01653153
Contributeur : Raphaël Rieu-Helft <>
Soumis le : vendredi 1 décembre 2017 - 10:04:47
Dernière modification le : jeudi 11 janvier 2018 - 02:01:56

Fichier

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

Identifiants

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

Partager

Métriques

Consultations de la notice

34

Téléchargements de fichiers

10