| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Depth-First Search and Strong Connectivity in Coq
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.
Cited literature [8 references]
https://hal.inria.fr/hal-01096354
Contributor : David Baelde Connect in order to contact the contributor
Submitted on : Wednesday, December 17, 2014 - 12:38:08 PM
Last modification on : Thursday, February 3, 2022 - 11:18:43 AM
Long-term archiving on: : Monday, March 23, 2015 - 3:00:51 PM
Contributor : David Baelde Connect in order to contact the contributor
Submitted on : Wednesday, December 17, 2014 - 12:38:08 PM
Last modification on : Thursday, February 3, 2022 - 11:18:43 AM
Long-term archiving on: : Monday, March 23, 2015 - 3:00:51 PM
File
jfla15_submission_2.pdf
Files produced by the author(s)