《可信软件的前沿理论和技术.ppt》由会员分享，可在线阅读，更多相关《可信软件的前沿理论和技术.ppt（5页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、可信软件的前沿理论和技术 Still waters run deep.流静水深流静水深,人静心深人静心深 Where there is life,there is hope。有生命必有希望。有生命必有希望课课 程程 简简 介介教学目标和基本要求教学目标和基本要求通过介绍通过介绍高可信软件研究领域中的国际前沿的理论和技术高可信软件研究领域中的国际前沿的理论和技术中科大耶鲁高可信软件联合研究中心的相关研究中科大耶鲁高可信软件联合研究中心的相关研究使同学们使同学们对高可信软件研究领域的理论和技术有初步了解对高可信软件研究领域的理论和技术有初步了解参与（至少是关注）该领域的研究和开发工作参与（至少是关
2、注）该领域的研究和开发工作并激发同学们从事科研工作的热情并激发同学们从事科研工作的热情课课 程程 简简 介介课程主要内容课程主要内容预备知识预备知识可信软件研究领域的快速、全面的评述（邵中可信软件研究领域的快速、全面的评述（邵中,1）函数式编程语言、函数式编程和验证（陈意云函数式编程语言、函数式编程和验证（陈意云,1）程序验证的逻辑基础（邵中、郭宇，程序验证的逻辑基础（邵中、郭宇，2）前沿专题前沿专题出具证明编译器的构造技术（陈意云，出具证明编译器的构造技术（陈意云，3）高可信软件中的自动定理证明技术（李兆鹏，高可信软件中的自动定理证明技术（李兆鹏，4）并行程序验证的理论和方法（张昱，并行程序
3、验证的理论和方法（张昱，5）国际上相关研究介绍（邵中，国际上相关研究介绍（邵中，6和和7）课课 程程 简简 介介课程实践安排：五个专题课程实践安排：五个专题用用SML语言编写函数式程序（庄重，语言编写函数式程序（庄重，1）用定理证明辅助工具用定理证明辅助工具Coq学习逻辑推理（王僖学习逻辑推理（王僖,2）用用Coq学习函数式程序的验证（张昊中，学习函数式程序的验证（张昊中，3）用用Coq完成一个简单的命令式程序的验证完成一个简单的命令式程序的验证 （蒋信（蒋信予，予，4和和5）用一阶逻辑定理可满足性检查器用一阶逻辑定理可满足性检查器Z3和出具证明编译和出具证明编译器器Ccomp进行定理证明和程
4、序验证（庄重，进行定理证明和程序验证（庄重，6）由联合研究中心的博士生指导课程实践由联合研究中心的博士生指导课程实践课程实践地点：电三楼课程实践地点：电三楼517机房，机房，14:00开始开始课课 程程 简简 介介课程考查课程考查没有考试，有课程实践考查没有考试，有课程实践考查每天（最后一天除外）下午有练习题，经助教验收每天（最后一天除外）下午有练习题，经助教验收后给出等级区分：优、良、中、差后给出等级区分：优、良、中、差根据各天的考查成绩给出本课程的成绩根据各天的考查成绩给出本课程的成绩本课程不同于平时的课程本课程不同于平时的课程欢迎课堂上发问欢迎课堂上发问欢迎课后讨论欢迎课后讨论欢迎加入联合研究中心欢迎加入联合研究中心