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