Réduction du nombre de variables en analyse de relations linéaires

This thesis takes place in automatic verification of numerical properties, mainly for embeded softwares. During verification one must represents in a finished way possibly infinite sets of values, for that a solution is use of convex polyhedra. This representation is precise but expensive so maximal number of variables is limited. The goal of this thesis is to increase the maximum number of variables which it is possible to represent. Two approaches were considered then tested. First we wanted to benefit from the presence of linear equations to eliminate a variable by equation. This approach appeared, in experiments, rather disappointing. Another apprroach, more promising, isthe use of cartesian product. The idea is then to represent independently the variables whose evolution is not dependent. This decomposition can be improved through a change of basis. An analyser wasdone in order to test these two approaches.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