2009年9月3日至5日，应中科大-耶鲁高可信软件联合中心的邀请，法国国家信息与自动化研究院（INRIA）的Yves Bertot研究员来到中科大苏州研究院，对中科大-耶鲁高可信软件联合中心进行访问。期间, Yves Bertot研究员讲授了定理证明工具Coq以及如何利用Coq对程序设计语言的语义进行形式化描述并进行静态分析。联合中心博士后郭宇和李兆鹏、博士生付明分别就中心当前开展的项目: 操作系统验证、出具证明编译器、并发程序验证进行了介绍。Yves Bertot研究员与中心部分师生进行了深入的探讨。

    Coq是著名的高阶定理证明辅助工具，在定理证明领域具有很高的地位。中科大-耶鲁高可信软件联合中心的多个项目都以Coq作为重要的定理证明和形式化描述工具。通过此次来访, 加深了联合中心师生对定理证明和形式化描述的理解, 更好地了解了国外相关领域的工作。

 

Yves Bertot研究员介绍工作

 

Yves Bertot研究员与我院中科大-耶鲁高可信软件联合中心部分师生合影

    Yves Bertot是法国国家信息与自动化研究院(INRIA) Sophia Antipolis研究中心的高级研究员。他的主要研究兴趣是用定理证明工具来形式化描述算法和数学理论。他对高阶定理证明辅助工具Coq有相当深入的了解, 著有Coq in a Hurry、Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions等书, 这些书是每个深入了解Coq的人必读的书目。目前Yves Bertot正带领开展Marelle项目, 该项目的目标是研究和使用在计算机上检验保证软件正确性的数学证明的相关技术，开发一些方法和工具以便从对数据、算法及其性质的精确描述和这些性质的证明产生正确的程序。