Gagnez sur tous les tableaux

National audienceNous vérifions automatiquement des programmes impératifs d'énumération destructures combinatoires implantées dans des tableaux satisfaisant despropriétés structurelles données. Ces programmes C sont spécifiés en ACSL etvérifiés avec la plateforme Frama-C. La vérification déductive démontreautomatiquement que tous les tableaux produits satisfont leurs propriétésstructurelles. Elle est facilitée par sa combinaison avec des analysesdynamiques, qui permettent aussi de valider d'autres propriétés des programmes,comme leur exhaustivité. Nous proposons une bibliothèque de programmes vérifiéset des patrons de programmation et de spécification facilitant leur conceptionet leur mise au point. Ces programmes trouvent une application naturelle dansle test exhaustif borné de programmes manipulant ces tableaux