Vérification formelle de programmes de génération de données structurées

International audienceCe document résume les travaux de recherche de ma thèse d’informatique intitulée “Vérification formelle de programmes de génération de données structurées”, dirigée depuis septembre 2012 par O. Kouchnarenko, professeur et co-encadrée par A. Giorgetti, maître de conférences.Les méthodes du génie logiciel, telles que la spécification formelle et la preuve déductive, rendent la conception de programmes plus rationnelle, augmentent leur qualité et accroissent la confiance du développeur dans la correction de sa production. En raison de leur fort coût, ces méthodes n’ont longtemps été appliquées que dans des domaines à fort enjeu de sûreté ou de sécurité. De nombreuxprogrès récents rendent ces pratiques vertueuses accessibles à d’autres domaines du développement logiciel.Par différentes études de cas, ce travail de thèse évalue la faisabilité de démonstrations automatiques de programmes manipulant des tableaux d’entiers. Le cadre d’investigation choisi est le domaine de la combinatoire énumérative car il fournit de nombreux algorithmes dont la difficulté et la structure sont bien adaptées aux capacités des prouveurs actuels. Dans la combinatoire, les efforts de formalisation et de démonstration se sont concentrés sur certains objets, appelés cartes.La combinatoire est la partie des mathématiques discrètes qui étudie des ensembles finis ou dénombrables d’objets appelés structures combinatoires. Les permutations de n objets distinguables et les permutations particulières, telles que les involutions, sont des exemples de structures combinatoires.La combinatoire énumérative propose des algorithmes pour générer ces structures et pour compter le nombre de structures composées d’un nombre donné d’éléments. Le lecteur désirant davantage de précisions peut par exemple se référer à [Sta97].Les cartes sont des objets mathématiques qui apparaissent naturellement dans l’étude de nombreux problèmes, de nature mathématique ou physique. Une carte (combinatoire) étiquetée est un triplet (D,R,L) où D est un ensemble fini à 2n éléments (pour un entier naturel n &gt= 0), appelés étiquettes ou brins, R est une permutation surD et L est une involution sans point fixe surD, telles que le groupe hR,Li engendré par R et L agit transitivement sur D [LZ04]. L’action transitive des permutations R et L correspond au fait que deux brins quelconques d’une carte peuvent être envoyés l’un sur l’autre par un nombre fini d’applications de R et L. Les combinatoriciens s’intéressent plus particulièrement aux cartes enracinées. Combinatorialement, une carte enracinée est une classe d’équivalence de cartes étiquetées isomorphes par les isomorphismes renommant leurs brins mais préservant l’un d’entre eux, appelé racine.Approches Formelles dans l’Assistance au D´eveloppement de Logiciels – AFADL’166