《513程序分析与程序验证.ppt》由会员分享，可在线阅读，更多相关《513程序分析与程序验证.ppt（13页珍藏版）》请在三一办公上搜索。
1、程序分析与程序验证,计算机科学技术系陈意云0551-,课 程 简 介,计算机科学的理论体系1、模型理论 关心的问题给定模型M，哪些问题可以由模型M解决如何比较模型的表达能力 经典计算确定的图灵机，可计算性理论属于模型理论 新型计算本质特点是交互(并发、分布、网络、网格、云)计算和交互的统一模型理论尚未出现,课 程 简 介,计算机科学的理论体系2、程序理论 关心的问题给定模型M，如何用模型M解决问题 包括的领域程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等,课 程 简 介,计算机科学的理论体系3、计算理论 关心的问题给定模型M和一类问题，解决该类问题需要多少资源 包
2、括的领域计算复杂性理论,课 程 简 介,作为编译原理的后续课程，可选内容列举：独立于机器的优化（涉及，但不是重点）依赖于机器的优化（留给高级系统结构课程）形式语义和类型论（程序设计语言理论课程）各种语言范型的实现技术（不涉及）提高软件质量的方法1、程序分析2、形式验证模型检测：对软件的数学模型进行系统地全面考察程序验证：用形式方法对软件进行数学推理,课 程 简 介,本课程概述学习程序分析和形式验证的基本原理，它们在高可信软件、代码优化、并行编译等许多方面有广泛应用学习和讨论各类方法解决的问题、采用的技术、理论特性、算法等，并说明这些方法之间的关系和不同。这些方法本身跨越多种程序设计语言特征,课
3、 程 简 介（程序分析原理）,什么是程序分析一种静态（如编译时）的技术，用于预测程序运行时动态布局或行为的一种安全（忠实于语义）且有效（所需时空少）的近似程序分析的应用编译时的代码优化，以避免冗余计算公共子表达式删除、无用赋值删除、循环优化一些静态分析工具，用于分析所关心的程序性质程序切片工具、安全性程序验证,课 程 简 介（程序分析原理）,集中在四种主要程序分析方式上数据流分析(data flow analysis)基于约束的分析(constraint based analysis)抽象解释(abstract interpretation)类型和结果系统(type and effect sy
4、stem)对每种方式描述主要原理，而不是技术的详细介绍怎样用到更复杂编程语言的分析,课 程 简 介（模型检测）,什么是模型检测验证系统满足性质（）的方法。它操作在系统的模型（语义）上，而不是在系统的描述（语法）上模型检测的应用常用于硬件和通信协议的验证中模型检测方法已经在工业界逐步得到应用，并且有一些较好的工具,课 程 简 介（模型检测）,集中在采用下面两种逻辑的方法上线性时态逻辑：时间是线性的逻辑计算树逻辑：时间可以分支的逻辑（时态逻辑：公式的真假不是静态的）模型检测的大体步骤由用户描述的一个模型开始判断用户所断言的假设在模型中是否有效若无效，则产生由执行轨迹构成的反例,课 程 简 介（程序
5、验证）,什么是程序验证将基于逻辑证明的方法用于程序性质的证明1、系统的描述是适当逻辑中的一组公式2、待证性质的规范是另一个公式3、验证就是通过该逻辑来证明 程序验证的应用对安全攸关的程序，验证所关心的性质软件的机械验证将改进软件的生产率、效率、reliability,课 程 简 介（程序验证）,程序验证的大体步骤程序员提供附加了适当断言的程序验证条件生成器为该程序产生验证条件定理证明器完成验证条件的证明涉及机械验证过程的各主要部分Hoare逻辑（公理语义）、最弱前条件演算从程序到定理 验证条件生成从定理到证明 自动定理证明,课 程 简 介,教材和参考书F.Nielson,H.R.Nielson
6、,and C.Hankin,Principles of Program Analysis,2nd edition,Springer,2005A.V.Aho,M.S.Lam,R.Sethi,and J.D.Ullman,Compilers:Principles,Techniques,and Tools,2nd edition,Addison-Wesley,2007M.Huth and M.Ryan,Logic in Computer Science:Modelling and Reasoning about Systems,Cambridge University Press,Second Edition,2004(有中译本)教学资源网页：http:/,
