"Cartes combinatoires" . . . . "The general problem of proving properties of imperative programs is undecidable. Some subproblems\u2013 restricting the languages of programs and properties \u2013 are known to be decidable. Inpractice, thanks to heuristics, program proving tools sometimes automate proofs for programs andproperties living outside of the theoretical framework of known decidability results. We illustrate thisfact by building a catalog of proofs, for similar programs and properties of increasing complexity. Mostof these programs are combinatorial map generators.Thus, this work contributes to the research fields of enumerative combinatorics and softwareengineering. We distribute a C library of bounded exhaustive generators of structured arrays, formallyspecified in ACSL and verified with the WP plugin of the Frama-C analysis platform. We also proposea testing-based methodology to assist interactive proof in Coq, an original formal study of maps, andnew results in enumerative combinatorics." . "Langage C" . . . "Frama-C" . . "Programmes imp\u00E9ratifs" . . "Preuve de programmes" . "Coq" . . "C (langage de programmation)" . "Formal verification of structured data generation programs" . . . . . "V\u00E9rification formelle de programmes de g\u00E9n\u00E9ration de donn\u00E9es structur\u00E9es" . "2016" . "Th\u00E8ses et \u00E9crits acad\u00E9miques" . . "V\u00E9rification formelle de programmes de g\u00E9n\u00E9ration de donn\u00E9es structur\u00E9es" . "ACSL" . "ACSL (langage de programmation)" . . "Text" . . . "D\u00E9bogage" . . . "Le probl\u00E8me g\u00E9n\u00E9ral de la preuve de propri\u00E9t\u00E9s de programmes imp\u00E9ratifs est ind\u00E9cidable. Pour deslangages de programmation et de propri\u00E9t\u00E9s plus restrictifs, des sous-probl\u00E8mes d\u00E9cidables sontconnus. En pratique, gr\u00E2ce \u00E0 des heuristiques, les outils de preuve de programmes automatisent despreuves qui sortent du cadre th\u00E9orique de ces sous-probl\u00E8mes d\u00E9cidables connus. Nous illustronscette r\u00E9ussite pratique en construisant un catalogue de preuves, pour des programmes et despropri\u00E9t\u00E9s de nature similaire et de complexit\u00E9 croissante. Ces programmes sont principalementdes g\u00E9n\u00E9rateurs de cartes combinatoires.Ainsi, ce travail contribue aux domaines de recherche de la combinatoire \u00E9num\u00E9rative et dug\u00E9nie logiciel. Nous distribuons une biblioth\u00E8que C de g\u00E9n\u00E9rateurs exhaustifs born\u00E9s de tableauxstructur\u00E9s, formellement sp\u00E9cifi\u00E9s en ACSL et v\u00E9rifi\u00E9s avec le greffon WP de la plateforme d\u2019analyseFrama-C. Nous proposons \u00E9galement une m\u00E9thodologie de test qui facilite la preuve interactive enCoq, une \u00E9tude formelle des cartes originale, et de nouveaux r\u00E9sultats en combinatoire \u00E9num\u00E9rative." . . .