CoqGraphs : Dijkstra Proofs in Coq


dec 25/2007 : The Proof of termination for the strongly connected components algorithm is ready and available (file [2]).


Started in 2007 With Simon Chemouil as part of an internship at INRIA under the supervision of Sylvain Conchon and Evelyne Contejean : A functor implementation of both Dijkstra’s algorithm and an algorithm of strongly connected components in COQ. A report on the subject is available in French (file [1]).


COQ 8.1 is required for this project see the COQ homepage for more information.

This project is based on the Coccinelle library.

The program scc-proof is released under the terms of the CeCILL-C licence.