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.