|
 
|
[DER15] Graphes et couplages en Coq
Conférence Nationale avec comité de lecture : Journées Francophones des langages applicatifs (JFLA), January 2015, pp.235-248, Val d'Ajol, France,Mots clés: Preuve formelle, graphes, Coq
Résumé:
Nous proposons une formalisation en Coq des graphes orientés et non orientés sans arête multiple. 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 {\oe}uvre efficacement les algorithmes de graphes.
Nous spécifions ensuite, à l'aide de cette bibliothèque, les notions de couplage et de couverture d'arêtes et développons un vérificateur formellement vérifié dont l'objectif est de certifier le résultat d'une fonction qui calcule un couplage de cardinalité maximale. 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 de cardinalité maximale.
BibTeX
| @inproceedings { | |||
| DER15, | |||
| title | = | "{Graphes et couplages en Coq}", | |
| author | = | " C. Dubois and S. Elloumi and B. Robillard and C. Vincent ", | |
| booktitle | = | "{Journées Francophones des langages applicatifs (JFLA)}", | |
| year | = | 2015, | |
| edition | = | "2015", | |
| month | = | "January", | |
| pages | = | "235-248", | |
| address | = | "Val d'Ajol, France", | |
| } | |||
