Abstract : Using Coq, we mechanize Wegener's proof of Kosaraju's linear-time algorithm for computing the strongly connected components of a directed graph. Furthermore, also in Coq, we define an executable and terminating depth-first search algorithm.
