Théorie des séquences adaptée à la vérification des programmes

Les choix de modèles sémantiques d'un langage de programmation ont un effet important sur l'efficacité de la vérification des programmes dans ce langage. En effet, de nombreuses techniques de vérification génèrent des formules mathématiques en utilisant ces modèles. Les théories mathématiques utilisées dans ces formules et leur forme ont un impact direct sur leur solvabilité par le solveur utilisé. La modélisation de la mémoire et des structures de données utilise souvent la théorie SMT (Satisfiabilité Modulo Théories) des tableaux qui est bien établie et utilisée dans le domaine des solveurs SMT. Dans cette théorie, les tableaux permettent d'associer des valeurs à des indices, quel que soit le type des indices ou des valeurs. La théorie permet également des opérations permettant d'écrire et de lire le contenu des tableaux. Cependant, dans les programmes concrets d'où viennent les formules à prouver, la mémoire et les structures de données sont généralement limitées. Par exemple, les tableaux dans les langages de programmation sont généralement indexés de 0 à une constante n. Bien qu'il soit envisageable d'encoder les tableaux finis dans la théorie SMT des tableaux, cela n'est pas toujours une solution satisfaisante, une raison étant que l'égalité extensionnelle sur un tableau fini de 0 à n, ne peut pas être directement modélisée en utilisant l'égalité extensionnelle sur des tableaux infinis qui considère tous les entiers. Une théorie SMT des séquences finies, dans laquelle les séquences sont des collections de valeurs indexées sur un ensemble contigu d'entiers, simplifierait la résolution des formules qui modélisent de telles structures de données. De plus, les séquences finies avec des opérateurs de concaténation et d'extraction peuvent également être utilisées pour exprimer des langages de spécification particuliers tels que la logique de séparation. Une difficulté est de choisir l'ensemble des opérations sur les séquences à supporter, puisque la décidabilité de la théorie en dépend. D'un autre côté, la décidabilité complète n'est pas toujours requise, car les formules obtenues par la vérification de programmes peuvent avoir une forme ou une utilisation spécifique des opérations. L'objectif de la thèse est d'étudier quelle théorie des séquences est appropriée pour la vérification de programmes. La thèse s'intéresse notamment au cas des séquences n-indexées, qui sont des séquences qui peuvent commencer à n'importe quel indice n et se terminer à n'importe quel indice m. Ces séquences sont no- tamment présentes dans le langage de program- mation Ada, mais étant une généralisation des séquences 0-indexées, elles devraient permettre de représenter et de raisonner sur ces dernières également. Dans cette thèse, une théorie des séquences n-indexées est proposée, et différentes façons de raisonner sur cette théorie sont ex- plorées, que ce soit à travers des axiomatisa- tions, en utilisant des théories existantes ou en développant différents calculi dédiés à cette théorie. L'évaluation de ces approches de raisonnement est effectuée à travers des implé- mentations en OCaml dans le solveur de con- traintes Colibri2. Divers détails de ces implé- mentations sont présentés, ainsi que des con- tributions supplémentaires apportées au raison- nement arithmétique.