Abstract FR:

L'analyse sémantique des variables numériques d'un programme consiste à déterminer statiquement et automatiquement des propriétés vérifiées par celles-ci à l'exécution. Différentes classes de propriétés (relations d'égalité, d'inégalité, de congruence) ont été étudiées. Cette thèse propose la généralisation d'une partie des modèles précédents. Plus particulièrement, en utilisant le cadre formel fourni par l'interprétation abstraite, nous proposons, d'une part, un ensemble de propriétés généralisant les intervalles et les classes de congruences entières et, d'autre part, une généralisation des trapézoïdes et des systèmes d'équation linéaires de congruence entières relationnelles. La définition d'une abstraction rationnelle de ces différentes propriétés permet d'obtenir des approximations, dont la complexité reste polynomiale en le nombre de variables considérées, des opérateurs sur les propriétés entières.