2017年信息安全新技术系列学术报告（第八期）

题目： A Semi-automatic Proof of Strong connectivity

学者： Jean-Jacques Lévy 教授

单位： Directeur de recherche émérite, Inria, France

时间： 12月15日 10:00—11:30

地点： 计控楼523室

Bio: Jean-Jacques Lévy graduated from the Ecole polytechnique in Paris, 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-2008) 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 debugging 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 (1998). He was a member of the research staff at DEC (1986-1988), and visiting professor at Iscas (2013-2014).

A Semi-automatic Proof of Strong connectivity

We present a formal proof of the classical Tarjan-1972 algorithm for finding strongly connected components in directed graphs. We use the Why3 system to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductive predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows the description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-of-the-art automatic provers and to manual interactive proof-checkers (we use mainly Coq). We do not claim that this proof is new, although we could not find a formal proof of that algorithm in the literature. But one important point of our article is that our proof is here completely presented and human readable.