可信软件的前沿理论和技术.ppt
《可信软件的前沿理论和技术.ppt》由会员分享,可在线阅读,更多相关《可信软件的前沿理论和技术.ppt(5页珍藏版)》请在三一文库上搜索。
1、可信软件的前沿理论和技术,计算机科学与技术学院 中科大耶鲁高可信软件联合研究中心 邵中、陈意云、张昱、郭宇、李兆鹏等,2010.7,课 程 简 介,教学目标和基本要求 通过介绍 高可信软件研究领域中的国际前沿的理论和技术 中科大耶鲁高可信软件联合研究中心的相关研究 使同学们 对高可信软件研究领域的理论和技术有初步了解 参与(至少是关注)该领域的研究和开发工作 并激发同学们从事科研工作的热情,课 程 简 介,课程主要内容 预备知识 可信软件研究领域的快速、全面的评述(邵中, 1) 函数式编程语言、函数式编程和验证(陈意云, 1) 程序验证的逻辑基础(邵中、郭宇,2) 前沿专题 出具证明编译器的构
2、造技术(陈意云,3) 高可信软件中的自动定理证明技术(李兆鹏,4) 并行程序验证的理论和方法(张昱,5) 国际上相关研究介绍(邵中,6和7),课 程 简 介,课程实践安排:五个专题 用SML语言编写函数式程序(庄重,1) 用定理证明辅助工具Coq学习逻辑推理(王僖, 2) 用Coq学习函数式程序的验证(张昊中,3) 用Coq完成一个简单的命令式程序的验证 (蒋信予,4和5) 用一阶逻辑定理可满足性检查器Z3和出具证明编译器Ccomp进行定理证明和程序验证(庄重,6) 由联合研究中心的博士生指导课程实践 课程实践地点:电三楼517机房,14:00开始,课 程 简 介,课程考查 没有考试,有课程实践考查 每天(最后一天除外)下午有练习题,经助教验收后给出等级区分:优、良、中、差 根据各天的考查成绩给出本课程的成绩 本课程不同于平时的课程 欢迎课堂上发问 欢迎课后讨论 欢迎加入联合研究中心,
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 可信 软件 前沿 理论 技术
链接地址:https://www.31doc.com/p-2589994.html