中科大－耶鲁高可信软件联合研究中心
简
介
一、概述
在中科大软件安全实验室和耶鲁大学FLINT实验室近五年合作的基础上，双方校长于2008年10月签署备忘录，以中科大软件安全实验室为基础，在中科大建立高可信软件联合研究中心。
该中心是在两校相关实验室多年合作的基础上建立的。五年多来，我校软件安全实验室在耶鲁大学邵中教授的指导（包括和他主持的FLINT实验室的合作）下，研究水平上升较快。在邵中教授的支持下，软件安全实验室多次获得国家基金面上项目的资助，目前正在合作申请“海外及港澳学者合作研究基金”。在国际会议和国内外期刊上，两校研究生共同发表了7篇论文，我校研究生单独发表论文10多篇。近6年在编程语言理论及实现技术、软件安全和软件形式验证等研究方向培养了18名博士，其中在高校当教师的有8人，在Intel、Microsoft和Sun公司研发部门工作的有6人，做博士后的有2人。
二、研究领域
（1）程序设计语言理论和实现技术。
这是一个持续活跃了半个世纪的研究领域，目前国际上最活跃的方向是并行编程语言的设计和实现技术、程序验证技术等。我们目前的研究集中在形式程序验证（formal program verification）和出具证明编译器（certifying compiler）两个方向上。通过近几年的国际合作研究，研究水平上升较快。
（2）第2步拟展开的研究方向是计算机网络方面。
有待耶鲁大学相关教授来访，和华蓓教授（可见htttp://staff.ustc.edu.cn/~bhua）和董群峰教授等经过充分交流后展开。
在高可信软件研究领域，联合研究中心以形式程序验证为主要方法，研究提高软件可信程度的理论和技术等，目前正在开展的课题有系统软件的形式验证、出具证明的编译器技术、并发多核软件的开发、自动定理证明系统等
在高可信软件研究领域，联合研究中心近5年的建设目标是：研究如何有效地集成形式程序验证和领域专用语言和逻辑（domain-specific languages and logics）这两种软件技术，形成提高编写高可信软件生产力、提高对它们正确性和安全性信任程度、并且能被工业界接受的软件开发新方法，构建基于此方法并能向工业界推广的开发携带证明大型系统软件的基础结构。这是一项为了把形式程序验证技术推向实用，解决其中理论和技术问题的奠基性研究。这项研究的成果将对提高安全攸关软件的可信度，对建设各种安全的信息系统有着重要作用。
三、研究团队
1、研究人员
目前在高可信软件及相关领域的研究人员如下： 教授：邵中、陈意云、华蓓、董群峰、冯新宇
副教授：张昱
博士后：郭宇、李兆鹏、付明
博士：华保健、郭燕
博士生和硕士生：20名左右
四、在高可信软件领域中的合作成果
1、近5年连续承担国家自然科学基金面上项目：
基于语言理论和实现技术的移动代码安全（Security of mobile code based on techniques of programming language theory and implementation）
类型论在软件安全方面的应用研究（Application Research of Type Theory in Software Security and Safety）
软件安全性的验证和编译（Verification and Compilation of Software Safety） 面向携带证明软件设计的语言、逻辑和证明（Languages, Logics, and Proofs for Certified Software Design）
2、近5年在编程语言理论及实现技术、软件安全和软件验证方面培养了14名博士，其中在Intel、Microsoft和Sun等公司研发部门工作的有6人，在高校当教师的有6人，做博士后的有2人。
3、近期发表的代表性论文如下：
[1] X.Feng, Z.Shao, A.Vaynberg, S.Xiang, and Z.Ni.Modular verification of aembly code with stack-based control abstractions.In Proc.2006 ACM Conference on Programming Language Design and Implementation, pages 401-414, June 2006.[2] Chunxian Lin, Andrew McCreight, Zhong Shao, Yiyun Chen, and Yu Guo.Foundational typed aembly language with certified garbage collection.In Proceedings of 1st IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, pages 326-335, IEEE CS pre, June 2007.[3] X.Feng, Z.Ni, Z.Shao, and Y.Guo.An open framework for foundational proof-carrying code.In Proc.2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation, pages 67-78, Jan.2007.[4] A.McCreight, Z.Shao, C.Lin, and L.Li.A General Framework for Certifying Garbage Collectors and Their Mutators.In Proc.2007 ACM Conference on Programming Language Design and Implementation, pages 468-479, June 2007.[5] X.Feng, Z.Shao, Y.Dong, and Y.Guo.Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.In Proc.2008 ACM Conference on Programming Language Design and Implementation, pages 170-182, June 2008.[6] X.Feng, Z.Shao, Y.Guo and Y.Dong.Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems.In Proc.Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments, October 2008.
五、欢迎加入联合研究中心
随着联合研究中心的正式成立，研究生导师、博士后和博士研究生的队伍都会逐步扩大。
欢迎对联合研究中心研究领域感兴趣的同学加入中心攻读博士学位。 经中国科学技术大学有关部门同意，联合研究中心面向国内外公开招聘研究生导师。招聘条件如下：
教授：具有博士学位，年龄不超过45周岁，在本领域取得了国内外同行所公认的学术成果，有指导博士研究生的能力。
副教授：具有博士学位，年龄不超过40周岁，有较大发展潜力，在本领域取得了一定的学术成绩，有指导研究生的能力。
招聘流程按照中国科学技术大学的规定，中国科学技术大学提供有竞争力的工作报酬和条件。
应聘者将个人简历、研究工作陈述和3位国内外同行专家推荐函，通过电子邮件发到kyhcs@ustc.edu.cn。联合研究中心经初步筛选后，推荐优秀者进入中国科学技术大学招聘流程。
此外，联合研究中心还招收博士后：年龄不超过35岁，在本领域取得了初步的学术成绩。
