CoqGraphs : Preuves et Dijkstra en Coq

Actualités

25 dec 2007 : La preuve de terminaison pour un algorithme de composantes fortement connectées est disponible (fichier [2]).

Description

Commencé en 2007 avec Simon Chemouil pendant un stage INRIA sous la supervision de Sylvain Conchon et Evelyne Contejean : Une implémentation fonctorisée de l’algorithme de Dijkstra et d’un algorithme de composantes fortement connectées en COQ. Un rapport sur le sujet est disponible en français (fichier [1]).

Notes

COQ 8.1 est requis pour ce projet. Regardez la page de Coq pour plus d’informations.

Ce projet est basé sur la librairie Coccinelle.

Le programme scc-proof est distribué sous les termes de la licence CeCILL-C.

Fichiers