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
Université Paris-Saclay (Espace Technologique, Bat. Discovery - RD 128 - 2e ét., 91190 Saint-Aubin - France)
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.
https://hal.inria.fr/hal-01099135
Contributor : Alain Giorgetti
<>
Submitted on : Monday, January 12, 2015 - 9:04:18 AM
Last modification on : Thursday, February 7, 2019 - 3:08:39 PM
Long-term archiving on : Saturday, September 12, 2015 - 1:25:17 AM
Richard Genestier, Alain Giorgetti, Guillaume Petiot. Gagnez sur tous les tableaux. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099135v2⟩
