可信软件前沿理论和技术.ppt_第1页
可信软件前沿理论和技术.ppt_第2页
可信软件前沿理论和技术.ppt_第3页
可信软件前沿理论和技术.ppt_第4页
可信软件前沿理论和技术.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开始,课 程 简 介,课程考查 没有考试，有课程实践考查 每天（最后一天除外）下午有练习题，经助教验收后给出等级区分：优、良、中、差 根据各天的考查成绩给出本课程的成绩 本课程不

人人文库> 全部分类> 教育资料 > 课件下载

温馨提示

  • 1. 本站所有资源如无特殊说明，都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等，如果需要附件，请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸，网页内容里面会有图纸预览，若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对用户上传分享的文档内容本身不做任何修改或编辑，并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容，请与我们联系，我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

最新文档

评论

0/150

提交评论