Formal proofs are usually very long. They are hardly checkable by humans, and the assistance of a computer is needed. Although it seems quasi impossible to read the details of the formal proof of a complex system, or an optimizing compiler, or an operating system or a many-cases program, one could envision possible to read the formal proofs of elegant but tricky algorithms with some help of automatic provers. In this talk, we take the examples of algorithms on graphs (depth-first-search, random-search, strongly connected components) and try to demonstrate that readability can be acheived modulo a bit of abstraction.

    Joint work with Chen Ran (Iscas), part of this work was presented at VSTTE 2017.

Bio：

    Jean-Jacques Levy graduated from the Ecole polytechnique in Paris, received a PhD from 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 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 has also been a member of the research staff at DEC (1986-1988), and visiting professor at Iscas (2013-2014).