九州手机版登录入口
 
新闻信息
新闻
教学信息
科研信息
学术活动
往期学术活动
通知公告
更多>>学术活动
您现在的位置:首页>新闻信息>新闻

法国Yves Bertot研究员访问中科大-耶鲁高可信软件联合中心

2010-06-10

  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项目, 该项目的目标是研究和使用在计算机上检验保证软件正确性的数学证明的相关技术,开发一些方法和工具以便从对数据、算法及其性质的精确描述和这些性质的证明产生正确的程序。


相关新闻
  • 法国Yves Bertot研究员访问中科大-耶鲁高可信软件联合中心

CopyRight 2009-2014 九州手机版登录入口_九州BET9手机登录入口 All Rights Reserved.
安徽省合肥市黄山路九州手机版登录入口西区电三楼
通信地址:安徽省合肥市4号信箱 九州手机版登录入口 邮政编码:230027