计算机科学技术系 陈意云 0551-3607043 yiyun@ustc.edu.cn 程序分析与程序验证 计算机科学技术系 陈意云 0551-3607043 yiyun@ustc.edu.cn.

Presentation on theme: "计算机科学技术系 陈意云 0551-3607043 yiyun@ustc.edu.cn 程序分析与程序验证 计算机科学技术系 陈意云 0551-3607043 yiyun@ustc.edu.cn."— Presentation transcript:

1 计算机科学技术系 陈意云 0551-3607043 yiyun@ustc.edu.cn
程序分析与程序验证 计算机科学技术系 陈意云

2 课 程 简 介 计算机科学的理论体系 1、模型理论  关心的问题 给定模型M，哪些问题可以由模型M解决 如何比较模型的表达能力
 经典计算 确定的图灵机，可计算性理论属于模型理论  新型计算 本质特点是交互( 并发、分布、网络、网格、云 )  计算和交互的统一模型理论尚未出现

3 课 程 简 介 计算机科学的理论体系 2、程序理论  关心的问题 给定模型M，如何用模型M解决问题  包括的领域
程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等

4 课 程 简 介 计算机科学的理论体系 3、计算理论  关心的问题 给定模型M和一类问题，解决该类问题需要多少资源  包括的领域
计算复杂性理论

5 课 程 简 介 作为编译原理的后续课程，可选内容列举： 独立于机器的优化（涉及，但不是重点） 依赖于机器的优化（留给高级系统结构课程）
形式语义和类型论（程序设计语言理论课程） 各种语言范型的实现技术（不涉及） 提高软件质量的方法 1、程序分析 2、形式验证 模型检测：对软件的数学模型进行系统地全面考察 程序验证：用形式方法对软件进行数学推理

6 课 程 简 介 本课程概述 学习程序分析和形式验证的基本原理，它们在高可信软件、代码优化、并行编译等许多方面有广泛应用
学习和讨论各类方法解决的问题、采用的技术、理论特性、算法等，并说明这些方法之间的关系和不同。这些方法本身跨越多种程序设计语言特征

7 课 程 简 介（程序分析原理） 什么是程序分析 程序分析的应用
一种静态（如编译时）的技术，用于预测程序运行时动态布局或行为的一种安全（忠实于语义）且有效（所需时空少）的近似 程序分析的应用 编译时的代码优化，以避免冗余计算 公共子表达式删除、无用赋值删除、循环优化 一些静态分析工具，用于分析所关心的程序性质 程序切片工具、安全性 程序验证

8 课 程 简 介（程序分析原理） 集中在四种主要程序分析方式上 对每种方式 数据流分析(data flow analysis)
基于约束的分析(constraint based analysis) 抽象解释(abstract interpretation) 类型和结果系统(type and effect system) 对每种方式 描述主要原理，而不是技术的详细介绍 怎样用到更复杂编程语言的分析

9 课 程 简 介（模型检测） 什么是模型检测 模型检测的应用
验证系统满足性质 （   ）的方法。它操作在系统的模型 （语义）上，而不是在系统的描述（语法）上 模型检测的应用 常用于硬件和通信协议的验证中 模型检测方法已经在工业界逐步得到应用，并且有一些较好的工具

10 课 程 简 介（模型检测） 集中在采用下面两种逻辑的方法上 模型检测的大体步骤 线性时态逻辑：时间是线性的逻辑
计算树逻辑：时间可以分支的逻辑 （时态逻辑：公式的真假不是静态的） 模型检测的大体步骤 由用户描述的一个模型开始 判断用户所断言的假设在模型中是否有效 若无效，则产生由执行轨迹构成的反例

11 课 程 简 介（程序验证） 什么是程序验证 程序验证的应用 将基于逻辑证明的方法用于程序性质的证明 1、系统的描述是适当逻辑中的一组公式
2、待证性质的规范是另一个公式 3、验证就是通过该逻辑来证明   程序验证的应用 对安全攸关的程序，验证所关心的性质 软件的机械验证将改进软件的生产率、效率、reliability

12 课 程 简 介（程序验证） 程序验证的大体步骤 涉及机械验证过程的各主要部分 程序员提供附加了适当断言的程序
验证条件生成器为该程序产生验证条件 定理证明器完成验证条件的证明 涉及机械验证过程的各主要部分 Hoare逻辑（公理语义）、最弱前条件演算 从程序到定理 —— 验证条件生成 从定理到证明 —— 自动定理证明

13 课 程 简 介 教材和参考书 F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis, 2nd edition, Springer, 2005 A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools , 2nd edition, Addison-Wesley, 2007 M. Huth and M. Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, Second Edition, 2004(有中译本) 教学资源网页：