Title: Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle 

　　Speaker: Jean-Jacques Lévy 

　　               Irif, Inria Paris 

　　Venue: Lecture Room of SKLCS, Room 337, Building 5 

　　Time: 3:00pm, Jul. 3rd, 2019, Wednesday 

　　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. 

　　Bio: 

　　JJL graduated from the Ecole Polytechnique, PhD at Univ. of Paris 7. He worked on optimal reductions in the lambda-calculus, on properties of term rewriting systems and on concurrency theory. He has been appointed as a professor of Computer Science at the Ecole polytechnique in Palaiseau 

　　(1992-2006) and as the managing director of the new Microsoft Research-INRIA Joint Centre in Paris (2006-2012). He is presently Senior Researcher emeritus at Inria in Univ. of Paris 7. His current research is on formal proofs of programs. He also participated to the static analysis of the embedded code of the Ariane 5 (after its explosion in 1996) and directed the review of the embedded code of the Columbus module of the ISS (1996). He was a member of the research staff at DEC (1986-1988) and visited professor at Iscas (2013-2014).