  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.
