Depth-First Search and Strong Connectivity in Coq

François Pottier (1)

1 GALLIUM - Programming languages, types, compilation and proofs

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.

Domaines: Logique en informatique [cs.LO]

François Pottier. Depth-First Search and Strong Connectivity in Coq. Vingt-sixièmes journées francophones des langages applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01096354⟩