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