Skip to Main content Skip to Navigation
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 metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-00812515
Contributor : Sandrine Blazy <>
Submitted on : Friday, April 12, 2013 - 11:46:33 AM
Last modification on : Friday, July 10, 2020 - 4:10:42 PM
Long-term archiving on: : Monday, April 3, 2017 - 4:36:42 AM

Files

paper.pdf
Files produced by the author(s)

Identifiers

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

Citation

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⟩

Share

Metrics

Record views

1320

Files downloads

369