Skip to Main content Skip to Navigation
Theses

Abstraction de traces en analyse statique et transformation de programmes.

Abstract : We study of abstractions for sets of traces adapted to static analysis and program transformations in the abstract interpretation framework. In the first part, we propose a general framework for control-based trace partitioning in static analysis. In particular, this framework allows to use properties of the history of program executions in order to express disjunctions of abstract properties in static analyses. As a result, we obtain e±cient analyses, improving not only precision but also execution time in most cases. This method was implemented in the Astree analyzer, devoted to the analysis of C programs. Moreover, we report excellent result in the analysis of large critical real world programs. In the second part, we develop automatic techniques for the inspections of alarms produced by an analyzer such as Astree. Indeed, the analyzer is incomplete, so an alarm raised by Astree could be either a real bug or just be due to an imprecision inherent in the analysis. First, we propose to extract semantic slices, i.e. subsets of the program execution traces, which satisfy some given conditions; this approach allows to characterize more precisely the context corresponding to an alarm. Furthermore, in some cases, it helps to prove the alarm to be false; otherwise, it may help to find a real error scenario. Then, we define families of dependence analyses so as to track the origin of abnormal behaviors in programs, and to help for a more efficient diagnosis of the reason why an alarm was raised. We got encouraging results using a prototype, which we implemented. In the last part, we define a general formalization for compilation in the abstract interpretation framework and we integrate several approaches to certified compilation in our framework. First, we propose a method based on a translation of abstract invariants computed in an analysis of the source code and on the checking of the the soundness of the resulting invariants. This checking allows to trust the translated invariant independently from any assumption about the soundness of the translation or the source analysis. Second, we formalize the translation equivalence approach, which amounts to proving the correctness of compilation, by checking that the source program and the compiled program are equivalent. Last, we compare both techniques not only in the theoretical point of view but also in a practical experiment.
Document type :
Theses
Complete list of metadatas

Cited literature [120 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/pastel-00001914
Contributor : Ecole Polytechnique <>
Submitted on : Thursday, July 29, 2010 - 4:47:29 PM
Last modification on : Thursday, October 29, 2020 - 3:01:41 PM
Long-term archiving on: : Thursday, November 4, 2010 - 10:11:38 AM

Identifiers

  • HAL Id : pastel-00001914, version 1

Collections

Citation

Xavier Rival. Abstraction de traces en analyse statique et transformation de programmes.. Informatique [cs]. Ecole Polytechnique X, 2005. Français. ⟨pastel-00001914⟩

Share

Metrics

Record views

709

Files downloads

456