Friday, 21. october 2005, 2PM / Vendredi 21 octobre 2005, 14h
Prepared in the Computer Science Department of the Ècole Normale Supérieure
Supervised by Patrick Cousot
Place/lieu: Amphi Gay Lussac, École Polytechnique (see the map/voir le plan)
Pot: Room 70, Paul Lévy Building, around 4PM/Salle 70, Batiment Paul Lévy, autour de 16h
In a first part, we propose the definition of trace partitioning domains, which allow to express and infer properties involving disjunction, based on control flow criteria. We set up a generic trace partitioning framework. The trace partitioning domain of the Astrée analyzer is a first instantiation of this framework. It allows for a great precision level to be obtained, by analyzing precisely the control flow paths in some part of programs. Yet, it does not incur a major cost in time or memory. A second instantiation is a technique related to synchronous product, which allows to express fine properties about program executions.
In a second part, we consider the problem of the investigation of the alarms raised by analyzers like Astrée. False alarms cannot be avoided, due to the undecidability of the problem of interest, which makes the investigation of alarms a relevant issue. We define semantic slices as subsets of the semantics of programs. A semantic slice can be approximated by invariants, computed by combination of forward and backward analyses. Semantic slicing criteria allow to focus on the dangerous executions, satisfying some conditions (input values, control flow history). We set up a definition of abstract dependences, which allow to track the dependences among specific properties, which allows to find out what the error behavior of a program depends on.
In a third part, we focus on certified compilation. We give a formalization for optimizing and non-optimizing compilation. Then, we study certification algorithms. Invariant translation techniques perform a traduction of invariants computed by a static analysis of the source code and produce invariants for the compiled programs. Invariant checking allows to make sure that the resulting invariant is sound independantly from any assumption about the compiler or about the source invariant. By contrast, translation validation checks that the compiled program is actually equivalent to the source code. We formalized, implemented and compared these techniques.
Dans une première partie, nous définissons un domaine de partitionnement de traces, qui permet d'exprimer et d'inférer des propriétés contenant des disjonctions, fondées sur des critères extraits du flot de contrôle. Nous proposons un cadre de travail pour définir de tels domaines. Le domaine de partitionnement de traces de Astrée est une instance de ce cadre. Ce domaine rend possible un très bon niveau de précision, en analysant précisément le flot de contrôle de certaines parties des programmes. Toutefois, le coût de ce domaine en temps et en mémoire est très raisonnable. Deuxièmement, une technique proche du produit synchrone est proposée, qui permet d'exprimer des propriétés plus fines à propos des traces d'exécution.
Dans une deuxième partie, nous nous intéressons à l'investigation d'alarmes levées par des analyseurs tels qu'Astrée. On ne peut pas éviter complètement l'occurence de fausses alarmes, en raison de l'indécidabilité des problèmes considérés, d'où la nécessité d'investiguer l'origine des alarmes. Nous appelons slice sémantique un sous ensemble de la sémantique du programme. Une telle slice peut être approximée par des invariants, calculés à l'aide de combinaisons d'analyses avant-arrière. Les slices sémantiques permettent de se restreindre aux traces dangereuses, satisfaisant certaines conditions (valeurs des entrées, histoire du flot de contrôle). Nous définissons des dépendances abstraites, qui permettent de rechercher de quoi l'occurence d'erreur dépend.
Dans une troisième partie, nous nous intéressons à la compilation certifiée. Nous donnons une formalisation pour la compilation optimisante et non optimisante. Ensuite, nous étudions des algorithmes de certification. Les techniques de traduction d'invariants utilisent un invariant calculé au niveau du programme source, afin de produire un invariant pour le programme compilé. La vérification de l'invariant traduit permet d'en prouver la correction indépendament de toute hypothèse de correction du compilateur ou de l'invariant initial. La vérification de traduction certifie l'équivalence du programme compilé et du programme source. Nous avons formalisé, implémenté et comparé ces techniques.