Gagnez sur tous les tableaux

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.