| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
Extracting a data flow analyser in constructive logic
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.
Cited literature [22 references]
https://hal.inria.fr/inria-00564611
Contributor : Mister Dart <>
Submitted on : Wednesday, February 9, 2011 - 2:28:17 PM
Last modification on : Saturday, January 9, 2021 - 3:40:34 AM
Long-term archiving on: : Tuesday, May 10, 2011 - 3:18:41 AM
Contributor : Mister Dart <>
Submitted on : Wednesday, February 9, 2011 - 2:28:17 PM
Last modification on : Saturday, January 9, 2021 - 3:40:34 AM
Long-term archiving on: : Tuesday, May 10, 2011 - 3:18:41 AM
File
extract-tcs.pdf
Files produced by the author(s)