Cette thµese est consacree à l'etude d'abstractions d'ensemble de traces adaptees µa l'analyse statique et aux transformations de programmes. Cette etude a ete menee dans le cadre de l'interpretation abstraite. Dans une premiµere partie, nous proposons un cadre general permettant de definir des analyses effectuant un partitionnement des traces. Cela permet en particulier d'utiliser des proprietes definies par l'histoire des executions, pou ecrire des disjonctions de proprietes abstraites utiles lors de l'analyse statique. Ainsi, nous obtenons des analyses plus efficaces, qui sont non seulement plus precises mais aussi plus rapides. La methode a ete implementee et eprouvee dans l'analyseur de code C Astree, et on obtient d'excellents resultats lors de l'analyse d'applications industrielles de grande taille. La seconde partie est consacree au developpement de methodes permettant d'automatiser le diagnostique des alarmes produites par un analyseur tel qu'Astree. En eff en raison de l'incompletude de l'analyseur, une alarme peut, soit reveler une veritable erreur dans le programme, soit provenir d'une imprecision de l'analyse. Nous proposons tout d'abord d'extraire des slices semantiques, c'est à ire des sous-ensembles de traces du programme, satisfaisant certaines conditions ; cette technique permet de mieux caracteriser le contexte d'une alarme et peut aider, soit àprouver l'alarme fausse, soit à montrer un veritable contexte d'erreur. Ensuite, nous definissons des familles d'analyses de dependances adaptees µa la recherche d'origine de comportements anormaux dans un programme, afin d'aider µa un diagnostique plus efficace des raisons d'une alarme. Les resultats lors de l'implementation d'un prototype sont encourageants. Enfin, dans la troisiµeme partie, nous definissons une formalisation generale de la compilation dans le cadre de l'interpretation abstraite et integrons diverses techniques de compilation certifiee dans ce cadre. Tout d'abord, nous proposons une methode fondee sur la traduction d'invariants obtenus lors d'une analyse du code source et sur la verification independante des invariants traduits. Ensuite, nous formalisons la methode de preuve d'equivalence, qui produit une preuve de correction de la compilation, en prouvant l'equivalence du programme compile et du programme source. Enfin, nous comparons ces methodes du point de vue theorique et µa l'aide de resultats experimentaux.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00001914 |
| Date | 21 October 2005 |
| Creators | Rival, Xavier |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds