Extracting a data flow analyser in constructive logic

David Cachera, Thomas P. Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, 342(1):56-78, 2005. [doi]

Abstract

A constraint-based data flow analysis is formalised in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract domains. Constraints are represented in a way that allows for both efficient constraint resolution and correctness proof of the analysis with respect to an operational semantics. 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 flow analyser in Ocaml from the proof. The library of lattices and the representation of constraints are defined in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq.

Available at http://hal.inria.fr/docs/00/56/46/11/PDF/extract-tcs.pdf