Extracting a data flow analyser in constructive logic - Archive ouverte HAL Access content directly
Journal Articles Theoretical Computer Science Year : 2005

Extracting a data flow analyser in constructive logic

David Cachera
Thomas Jensen
  • Function : Author
  • PersonId : 874110
David Pichardie


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.
Fichier principal
Vignette du fichier
extract-tcs.pdf (240.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00564611 , version 1 (09-02-2011)



David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, 2005, 342 (1), pp.56-78. ⟨10.1016/j.tcs.2005.06.004⟩. ⟨inria-00564611⟩
338 View
110 Download



Gmail Facebook Twitter LinkedIn More