Skip to Main content Skip to Navigation
New interface
Conference papers

Formal Verification of a C Value Analysis Based on Abstract Interpretation

Abstract : Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their implementation on real languages is still error-prone. This paper presents a formal verification using the Coq proof assistant: a formalization of a value analysis (based on abstract interpretation), and a soundness proof of the value analysis. The formalization relies on generic interfaces. The mechanized proof is facilitated by a translation validation of a Bourdoncle fixpoint iterator. The work has been integrated into the CompCert verified C-compiler. Our verified analysis directly operates over an intermediate language of the compiler having the same expressiveness as C. The automatic extraction of our value analysis into OCaml yields a program with competitive results, obtained from experiments on a number of benchmarks and comparisons with the Frama-C tool.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Friday, April 12, 2013 - 11:46:33 AM
Last modification on : Friday, November 18, 2022 - 9:26:10 AM
Long-term archiving on: : Monday, April 3, 2017 - 4:36:42 AM


Files produced by the author(s)


  • HAL Id : hal-00812515, version 1
  • ARXIV : 1304.3596


Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344. ⟨hal-00812515⟩



Record views


Files downloads