Abstract FR:

Cette thèse s'inscrit dans la vérification automatique de propriétés numériques de programmes, principalement des logiciels embarqués. Lors de la vérification on doit représenter de façon finie des ensembles éventuellement infinis de valeurs, pour cela une solution possible est l'utilisation de polyèdres convexes. Cette représentation est précise mais coûteuse ce qui limite le nombre de variables qu'il est possible de manipuler. Le but de cette thèse est d'augmenter le nombre maximal de variables qu'il est possible de représenter. Deux approches ont été envisagées puis testées. Dans un premier temps on a voulu tirer profit de la présence d'équations affines pour éliminer une variable par équation. Cette approche s'est révélée, expérimentalement, assez décevante. Une autre approche, bien plus prometteuse, est l'utilisation du produit cartésien. L'idée est alors de représenter indépendamment les variables dont l'évolution n'est pas liée. Cette décomposition peut être améliorée grâce à un changement de base. Un analyseur a été réalisé afin de tester ces deux approches.