Graphes et couplages en CoqReportar como inadecuado




Graphes et couplages en Coq - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 CEDRIC - Centre d-Etude et De Recherche en Informatique du Cnam

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.





Autor: Catherine Dubois - Sourour Elloumi - Benoit Robillard - Clément Vincent -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados