Extracting a data ow analyser in constructive logic

A constraint-based data ow analysis is formalised in the specication language of the Coq proof assistant. This involves dening a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract do-mains. Constraints are represented in a way that allows for both ecient constraint resolution and correctness proof of the analysis with respect to an operational se-mantics. The proof of existence of a solution to the constraints is constructive which means that the extraction mechanism of Coq provides a provably correct data ow analyser in Ocaml from the proof. The library of lattices and the representation of constraints are dened in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq. Key words: Program analysis; constructive logic; lattices; theorem proving; constraint solving