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項目, 該項目的目標是研究和使用在計算機上檢驗保證軟件正確性的數學證明的相關技術，開發一些方法和工具以便從對數據、算法及其性質的精確描述和這些性質的證明產生正確的程序。
