Formal Verification of a C Value Analysis Based on Abstract Interpretation

TL;DR

This paper formalizes and verifies a C value analysis based on abstract interpretation using Coq, ensuring soundness and integrating it into the CompCert compiler, with competitive experimental results.

Contribution

It introduces a formal Coq-based verification of a value analysis for C, including a soundness proof and integration into a verified compiler.

Findings

Verified analysis operates over an intermediate language with C expressiveness.

The mechanized proof uses translation validation of a Bourdoncle fixpoint iterator.

Experimental results show competitive performance compared to Frama-C.

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.