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

 
■  你相信自己的数学直觉吗？
 
你写下的证明真的可靠吗？

你理解各种数学证明技巧的原理吗？

你会用数学证明来自动生成计算机程序吗？ 

2011年8月13日至21日，第三届亚太地区形式化方法暑期学校，将教你学用世界著名的证明辅助工具Coq，感受数学与计算机结合的完美艺术！详情请见附件。

     日前，中科大－耶鲁高可信软件联合研究中心梁红瑾、冯新宇和付明的论文A Rely-Guarantee-Based Simulation for Verifying Concurrent Program Transformations被第39届 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages（简称POPL）录用。这是联合研究中心的研究迈入国际一流水平的里程碑。此前，中国大陆无任何单位以第一作者单位的身份在POPL上发表过论文。梁红瑾等的论文的发表，将使得中国科学技术大学成为大陆第一个以第一单位在POPL上发表论文的高校和科研院所，真正实现了“零的突破”。
     POPL是编程语言领域历史最久、水平最高的国际会议，它是讨论编程语言和编程系统最新突破的最主要论坛，内容涵盖编程语言的理论、编程语言的设计、编译器技术、程序分析、程序验证、可信软件等众多研究领域。国际期刊和会议的各种分区方法都把POPL放在该领域的最高区域中。

2011 年4月25 日，应中科大耶鲁高可信软件联合研究中心邀请，德国慕尼黑理工大学的Christian Urban博士来中科大苏州研究院访问。Christian Urban博士于2000年在英国剑桥大学获博士学位，随后在剑桥大学、普林斯顿大学和慕尼黑理工大学从事定理证明相关的研究工作。Christian Urban博士是著名定理证明器Isabelle的核心开发者之一，近年来主要关注自动定理证明、程序语言等理论领域。

 2011年5月11号，哥本哈根IT大学博士后Søren Debois博士来到联合研究中心进行了为期三天的学术访问和交流。Søren Debois博士于2008年在哥本哈根IT大学获得博士学位，他的主要研究内容围绕Bigraphs展开。目前，Søren Debois博士致力于研究程序语言，并发模型和普适系统之间的关系。访问期间，Søren Debois博士和研究中心的师生进行了深入的学术探讨，并对他的工作做了精彩的报告。

 会前冯老师向实验室师生介绍Søren Debois博士

The 3rd Asian-Pacific Summer School on Formal Methods will be held in Suzhou, China in August 13-21, 2011. The objective is to teach students the principles and practice of programming with the proof assistant Coq, as in previous years (2009 and 2010), and to show them the state of art applications of proof assistants and theorem provers in formal methods.
 

2010年12月16号，法国国家自动化研究院(INRIA)，中法信息自动化与应用数学联合实验室(LIAMA) 软件专家 Vania Joloboff 教授应中科大计算机学院冯新宇教授邀请，对科大耶鲁高可信软件联合中心进行学术访问，并就他目前所做的仿真器软件"SImSoC"做了精彩的报告。高可信中心的教授，博士后和博士硕士研究生参与了本次讲座。讲座现场气氛活跃，内容丰富生动，报告结束后，围绕中心的研究方向，现场师生踊跃提问，Joloboff教授一一做了详尽的解答。双方并就彼此的研究内容进行了深层次的探讨，大家收益甚多。

Joloboff教授正在和冯新宇教授以及陈意云教授探讨中

Joloboff正在给我们做报告

2010年11月25号，美国Lehigh大学计算机科学学院软件安全实验室(SOS)助理教授谭刚博士访问了联合研究中心。访问期间，谭刚博士具体介绍了自己的研究内容和研究方向，包括他目前正在参与的一个项目“GoNative”。该项目致力于在高级语言如C#,Java和Python中如何安全执行在程序代码中包含的低级语言代码片段。

关于这个报告更详细的内容，请点击此处。

谭刚博士

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作为重要的定理证明和形式化描述工具。通过此次来访, 加深了联合中心师生对定理证明和形式化描述的理解, 更好地了解了国外相关领域的工作。