题  目：Comparing a Formal Proof  in Why3, Coq, Isabelle

内容简介：In this talk we discuss how to publish formal proofs and formal proofs have to be checked by computer?

报告人：法国国家信息与自动化研究所  Jean-Jacques Lévy  研究员

报告人简介：Jean-JacquesLévy 乐俊杰，1968年本科毕业于法国综合理工大学；1978年博士毕业于巴黎大学； 1970-2012先后担任INRIA初级和高级研究员； 1992-2006任Palaiseau理工学院计算机科学教授； 2013-2014任中国科学院客座教授1984-1990先后担任 Xerox PARC（美国帕洛阿尔托）和DEC / SRC（帕洛阿尔托）的顾问。他先后在法国中央理工大学、巴黎第七大学开设过“算法与编程”、“计算机科学基础”、“信息基础”等研究生课程，曾在北京清华大学和布宜诺斯艾利斯大学（UBA）教授功能语言和程序验证课程。他历任法国萨克莱的新Microsoft Research-INRIA联合中心主任及巴黎数学科学科学理事会委员和三个欧洲项目的协调员。他在lambda算子的语法和语义及重写系统、并行计算理论、程序验证等方面取得系列成果，他参与了Ariane 5嵌入式软件的静态分析、图卢兹和DASA领导ISS哥伦布欧洲模块嵌入式代码的国际审查，为CNES和ESA的新编程规则做出突出贡献。他指导了20名优秀的博士生，发表了50篇论文，出版了6本书，共同实现了6种软件，并拥有1项美国专利。目前正研究用Why3，Coq和Isabelle / HOL系统证明图算法的正确性。

时  间：2019年11月18日（周一）上午10：30始

地  点：南海楼224室

热烈欢迎广大师生参加!

信息科学技术学院

2019年11月12日