研究方向、研究课题和研究团队简介.doc

研究方向、研究课题和研究团队简介 一、主要研究方向软件的依赖程度日益增长rusted computing base，简称TCB），将编译器等软件排除在TCB的外面。 近10年来，许多程序逻辑和类型系统已经被建议用于复杂软件的形式验证，相应的编程语言和编译器技术被用来为低级语言程序出具安全性或正确性的证明。它们致力于不同的抽象层次，使用不同的规范语言和公理，强调不同的语言特征和性质。 我们研究团队在这方面开展的一些研究工作可见网站/。 二、当前正在进行和近期已完成的主要研究课题 1、高可信软件中的形式程序验证（国家自然科学基金项目） 2、内存一致性模型的通用描述及验证框架（国家自然科学基金项目） 3、构建高可信软件中的自动定理证明问题研究 三、研究团队 上述研究方向的研究团队见下面，该团队是中科大－耶鲁高可信软件联合研究中心的重要组成部分，在校本部和苏州研究院两地有研究基地。研究生在该团队的共同指导和关注下开展工作。 ( 教授：邵中（耶鲁大学，我校大师讲席教授）、冯新宇、陈意云 ( 副教授：张昱、郭宇、李兆鹏、梁红瑾 ( 博士后：付明 ( 博士生和硕士生：20名左右 对上述方向感兴趣的同学可以选择邵中教授、冯新宇教授或张昱副教授等作为导师。本人不直接招收研究生，将作为团队的成员共同指导。 邵中教授是耶鲁大学教授、中国科大大师讲席教授、兼职博士生导师。他的科研工作和成果简介如下： 是学术界和工业界科研项目中广泛使用的SML/NJ函数式编程语言的编译器的主要设计和实现者之一，其中有影响的研究成果包括基于后续传递风格的编译方法等多项成果。 研究和开发了保类型的编译器基础构造FLINT，其中最显著的贡献是用高阶lambda演算对多种差异明显的源语言的类型系统进行编码，使得类型检查可以在编译的任何阶段进行。 近年来，研究重点集中在开发新的程序验证理论和技术，目标是为开发经过验证的大规模系统软件构建一种实用的基础平台。提出了领域专用语言加领域专用逻辑来验证领域专门代码并连接它们成为完整的经过验证的软件系统的思想和方法。已经开创性地设计了验证操作系统若干部分所需的多种专用逻辑和连接各种证明的开放框架，完成了汇编代码级的垃圾收集和存储分配等库函数、自修改代码的引导程序、非抢占式并发线程等实例程序的验证，最近验证了一个带硬中断和抢占式并发的简单操作系统。 四、对研究生的希望和要求 ( 树立社会主义荣辱观，有社会责任感。 ( 有学习理论和从事科研的兴趣，有开拓进取精神、工作责任心、团队意识等。 ( 在数学、逻辑、程序设计语言