Gagnez sur tous les tableaux

Richard Genestier 1 Alain Giorgetti 2, 1 Guillaume Petiot 1, 3
1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Résumé : Nous vérifions automatiquement des programmes impératifs d'énumération de structures combinatoires implantées dans des tableaux satisfaisant des propriétés structurelles données. Ces programmes C sont spécifiés en ACSL et vérifiés avec la plateforme Frama-C. La vérification déductive démontre automatiquement que tous les tableaux produits satisfont leurs propriétés structurelles. Elle est facilitée par sa combinaison avec des analyses dynamiques, qui permettent aussi de valider d'autres propriétés des programmes, comme leur exhaustivité. Nous proposons une bibliothèque de programmes vérifiés et des patrons de programmation et de spécification facilitant leur conception et leur mise au point. Ces programmes trouvent une application naturelle dans le test exhaustif borné de programmes manipulant ces tableaux.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01099135
Contributeur : Alain Giorgetti <>
Soumis le : lundi 12 janvier 2015 - 09:04:18
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : samedi 12 septembre 2015 - 01:25:17

Fichier

jfla15-version2hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01099135, version 2

Collections

CEA | INRIA | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | JFLA2015 | UNIV-LORRAINE | DRT | CEA-UPSAY | LORIA-FM | LORIA | UNIV-PARIS-SACLAY | LIST

Citation

Richard Genestier, Alain Giorgetti, Guillaume Petiot. Gagnez sur tous les tableaux. David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉. 〈hal-01099135v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

381

Téléchargements de fichiers

98

Contact


archive-ouverte@inria.fr