three formal proofs of tarjan’s strongly connected components algorithm in directed graphs
published：2019-11-12
title: three formal proofs of tarjan’s strongly connected components algorithm in directed graphs
time： 09:30-10:30, november14 thursday,2019
location: room 1002, science building b
lecturer：prof. jean-jacques levy (inria paris & irif)
abstract:
comparing provers on a formalization of the same problem is always a valuable exercise. in this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: why3, coq, and isabelle.
joint work with ran chen, cyril cohen, stephan merz and laurent théry presented at itp 2019.
links: