Extracting a data flow analyser in constructive logic

David Cachera 1 Thomas Jensen 1 David Pichardie 1 Vlad Rusu 2
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
2 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
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.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2005, 342 (1)
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

Contributeur : Mister Dart <>
Soumis le : mercredi 9 février 2011 - 14:28:17
Dernière modification le : jeudi 17 mai 2018 - 12:52:03
Document(s) archivé(s) le : mardi 10 mai 2011 - 03:18:41


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00564611, version 1


David Cachera, Thomas Jensen, David Pichardie, Vlad Rusu. Extracting a data flow analyser in constructive logic. Theoretical Computer Science, Elsevier, 2005, 342 (1). 〈inria-00564611〉



Consultations de la notice


Téléchargements de fichiers