dec 25/2007 : The Proof of termination for the strongly connected components algorithm is ready and available (file ).
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 ).
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.