中科大-耶鲁 高可信软件联合研究中心

2010年5月19日上午，邵中教授在3124教室作了题为“Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software”的学术报告。报告会由计算机科学与技术学院陈意云教授主持，来自07级的计算机学院本科生和其他感兴趣的部分师生参加了报告会。

邵中教授以纽约时报关于“近30年来改变人类生活的最重要的创新”的调查报导引出报告，该调查结果显示这些创新大都完全或部分地与计算机相关，如互联网、PC和膝上计算机、电子邮件、多处理器等。计算机相关的研究成果已广泛应用于并影响着人类生活的各个领域，但是，目前计算机系统资源（如处理器）的利用率不高、众多软件以至整个计算机系统的安全性面临挑战等现状导致人类社会期待着更多计算机研究和技术的创新，也给计算机学科的学生和科研人员带来了众多需要研究解决的问题。邵中教授由衷地指出：“现在学计算机的真是幸运的一代！”这激起了在座听众的热情和兴趣。

2009年11月18日，中法信息、自动化与应用数学联合实验室（LIAMA）主任Jean-Pierre Jouannaud教授与研究员Pierre-yves Strub 博士在科大耶鲁高可信软件联合中心进行为期两天的学术交流。LIAMA是法国国家信息与自动化研究所（INRIA）与清华大学等国内高校合作的联合实验室。本实验室介绍了联合中心以及目前正在开展的项目，博士后郭宇和李兆鹏分别介绍了操作系统内核验证与出具证明编译器的相关工作。

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