合作交流 / 学术报告

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