Return to search

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

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

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00012143
Date18 May 2005
CreatorsMerchat, David
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.002 seconds