Skip to Main content Skip to Navigation
Conference papers

Graphes et couplages en Coq

Résumé : Nous proposons une formalisation en Coq des graphes orientés et non orientés et des notions associées. La bibliothèque développée offre non seulement l'expressivité requise pour exprimer et démontrer des propriétés sur les graphes mais aussi une implantation purement fonctionnelle permettant de mettre en oeuvre efficacement les algorithmes de graphe. Nous spécifions ensuite à l'aide de cette bibliothèque les notions de couplage et d'ensemble de sommets couvrant et développons un vérificateur formellement vérifié dont l'objectif est de certifier le résultat d'un fonction qui calcule un couplage maximal. Le code exécutable de ce vérificateur est obtenu grâce au mécanisme d'extraction de Coq. Ce travail est une première contribution d'un projet plus ambitieux qui concerne le développement d'un algorithme de filtrage formellement vérifié pour la contrainte de différence (alldiff) pour des domaines finis. Ce dernier algorithme utilise de nombreuses manipulations de graphe dont le calcul d'un couplage maximal.
Document type :
Conference papers
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01099140
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:47:31 PM
Last modification on : Friday, January 17, 2020 - 5:06:01 PM
Long-term archiving on: : Saturday, April 15, 2017 - 12:23:55 PM

File

jfla15_submission_36.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01099140, version 1

Collections

Citation

Catherine Dubois, Sourour Elloumi, Benoit Robillard, Clément Vincent. Graphes et couplages en Coq. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099140⟩

Share

Metrics

Record views

155

Files downloads

380