|
|
|
| 通知公告 |
| 学术报告Formal Proof of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq, and Isabelle
|
报计算机软件新技术国家重点实验室
摘 要：
Comparing provers on a formalization of the same problem is always a valuable exercise. In this talk, 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.
告人简介:
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).
时间：6月26日(星期三) 10:00
地点：计算机科学技术楼203室
|
|
|
|
当前位置：首页 > 新闻中心 > 通知公告