[07.03]-Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle

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).