Résumé: Nous proposons dans cette thèse une technique d'analyse sémantique statique des programmes c élaborée a partir de l'évaluation partielle et de l'évaluation symbolique. La première méthode consiste a réduire un programme en fixant la valeur d'un sous-ensemble de ses paramètres pour obtenir un programme résiduel ayant la même sémantique que l'original pour ces valeurs ; la seconde consiste a évaluer le programme en propageant dans son code des symboles de valeurs donnes arbitrairement a ses variables d'entrée. L'évaluation partielle symbolique (eps) que nous proposons est une synthèse de ces deux méthodes. Son but est non seulement de vérifier statiquement la sémantique d'un programme c donne, en détectant statiquement des erreurs run-time comme dans l'évaluation symbolique, mais également de calculer un programme résiduel dont la sémantique est une abstraction de celle du programme original (et non pas une sémantique équivalente comme dans le cas de l'évaluation partielle). Cette méthode présente le caractère statique (off-line) de l'évaluation partielle et le caractere flow sensitive de l'évaluation symbolique. Ainsi l'intérêt du programme résiduel est double: d'une part sa représentation est débarrassée de tout ce qui ne contribue pas directement a sa sémantique, d'autre part chacun de ses chemins d'exécutions possibles est distingué des autres ; ainsi il se prête a diverses utilisations ultérieures, par exemple d'autres analyses ou des séries de tests, une bonne partie du travail étant alors déjà effectuée.

Paris:
Langue: Français
Collation: 216 p. ill. ;30 cm
Diplôme: Doctorat
Etablissement de soutenance: Paris, Université Paris et Marie Curie
Spécialité: Informatique
Thème Informatique

Note: Annexe pp.173-210; Bibliogr.pp.211-216