Gagnez sur tous les tableaux

Nous verifions automatiquement des programmes imperatifs d'enumeration de structures combinatoires implantees dans des tableaux satisfaisant des proprietes structurelles donnees. Ces programmes C sont specifies en ACSL et verifies avec la plateforme Frama-C. La verification deductive demontre automatiquement que tous les tableaux produits satisfont leurs proprietes structurelles. Elle est facilitee par sa combinaison avec des analyses dynamiques, qui permettent aussi de valider d'autres proprietes des programmes, comme leur exhaustivite. Nous proposons une bibliotheque de programmes verifies et des patrons de programmation et de specification facilitant leur conception et leur mise au point. Ces programmes trouvent une application naturelle dans le test exhaustif borne de programmes manipulant ces tableaux.