11月14日： jean-jacques levy
发布时间：2019-11-12 浏览量：17794
报告题目：three formal proofs of tarjan’s strongly connected components algorithm in directed graphs
报告人：prof. jean-jacques levy (inria paris & irif)
报告时间：2019年11月14日 周四 09:30 – 10:30
报告地点：理科大楼b1002
报告摘要：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.
joint work with ran chen, cyril cohen, stephan merz and laurent théry presented at itp 2019.
快速通道: