Skip to Main content Skip to Navigation

Verified static analyzes for low-level languages

Abstract : Static analysis of programs enables to study the possible behaviours of programs without running them. Static analysers may be used to guarantee that the execution of a program cannot result in a run-time error. Such analysis tools are themselves programs: they may have bugs. So as to increase the confidence in the results of an analysis, we study in this thesis how the implementation of static analysers can be formally proved correct. In particular, we build abstract interpreters within the Coq proof assistant and prove them correct. Namely, we formally establish that analysis results characterize all possible executions of the analysed program. Such abstract interpreters are integrated to the formally verified CompCert compiler, when relevant ; this enables to guarantee that safety properties that are proved on source code also hold for the corresponding compiled code. We focus on the analysis of programs written in low-level languages. Namely, languages which feature little or no abstractions (variables, functions, objects, types…) or abstractions that the programmer is allowed to break. This hampers the task of a static analyser which thus cannot rely on these abstractions to yield precise results. We discuss in particular how to automatically recover the control-flow graph of binary self-modifying programs, and how to automatically prove that a program written in C (in which pointer arithmetic is pervasive) cannot produce a run-time error.
Document type :
Complete list of metadata

Cited literature [94 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Wednesday, March 9, 2016 - 3:08:10 PM
Last modification on : Tuesday, October 20, 2020 - 4:42:02 PM
Long-term archiving on: : Monday, June 13, 2016 - 8:51:10 AM


Version validated by the jury (STAR)


  • HAL Id : tel-01285624, version 1


Vincent Laporte. Verified static analyzes for low-level languages. Programming Languages [cs.PL]. Université Rennes 1, 2015. English. ⟨NNT : 2015REN1S078⟩. ⟨tel-01285624⟩



Record views


Files downloads