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.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01099140
Contributeur : David Baelde <>
Soumis le : mercredi 31 décembre 2014 - 15:47:31
Dernière modification le : jeudi 13 septembre 2018 - 15:24:05
Document(s) archivé(s) le : samedi 15 avril 2017 - 12:23:55

Fichier

jfla15_submission_36.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01099140, version 1

Collections

Citation

Catherine Dubois, Sourour Elloumi, Benoit Robillard, Clément Vincent. Graphes et couplages en Coq. David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉. 〈hal-01099140〉

Partager

Métriques

Consultations de la notice

108

Téléchargements de fichiers

143