课程简介 计算机科学的理论体系 1、模型理论 ●关心的问题 -给定模型M, 哪些问题可以由模型M解决 -如何比较模型的表达能力 经典计算 确定的图灵机，可计算性理论属于模型理论 新型计算 本质特点是交互（并发、分布、网络、网格、云〉 ·计算和交互的统一模型理论尚未出现
课 程 简 介 计算机科学的理论体系 1、模型理论 • 关心的问题 – 给定模型M，哪些问题可以由模型M解决 – 如何比较模型的表达能力 • 经典计算 – 确定的图灵机，可计算性理论属于模型理论 • 新型计算 – 本质特点是交互( 并发、分布、网络、网格、云 ) • 计算和交互的统一模型理论尚未出现
课程简介 计算机科学的理论体系 2、程序理论 。关心的问题 -给定模型M, 如何用模型M解决问题 ●包括的领域 -程序设计范型、 程序设计语言、程序设计、形式 语义、类型论、程序验证、程序分析等
课 程 简 介 计算机科学的理论体系 2、程序理论 • 关心的问题 – 给定模型M，如何用模型M解决问题 • 包括的领域 – 程序设计范型、程序设计语言、程序设计、形式 语义、类型论、程序验证、程序分析等
课程简介 计算机科学的理论体系 3、计算理论 。关心的问题 给定模型M和一类问题，解决该类问题需要多少 资源 ●包括的领域 一计算复杂性理论
课 程 简 介 计算机科学的理论体系 3、计算理论 • 关心的问题 – 给定模型M和一类问题，解决该类问题需要多少 资源 • 包括的领域 – 计算复杂性理论
课程简介 作为编译原理的后续课程，可选内容列举： 独立于机器的优化（涉及，但不是重点》 一依赖于机器的优化（留给高级系统结构课程〉 -形式语义和类型论（程序设计语言理论课程） 各种语言范型的实现技术（不涉及》 一提高软件质量的方法 1、程序分析 2、形式验证 模型检测：对软件的数学模型进行系统地全面考察 程序验证：用形式方法对软件进行数学推理
课 程 简 介 作为编译原理的后续课程，可选内容列举： – 独立于机器的优化（涉及，但不是重点） – 依赖于机器的优化（留给高级系统结构课程） – 形式语义和类型论（程序设计语言理论课程） – 各种语言范型的实现技术（不涉及） – 提高软件质量的方法 1、程序分析 2、形式验证 模型检测：对软件的数学模型进行系统地全面考察 程序验证：用形式方法对软件进行数学推理
课程简介 本课程概述 学习程序分析和形式验证的基本原理，它们在高 可信软件、代码优化、并行编译等许多方面有广 泛应用 学习和讨论各类方法解决的问题、采用的技术、 理论特性、算法等，并说明这些方法之间的关系 和不同。这些方法本身跨越多种程序设计语言特 征
课 程 简 介 • 本课程概述 – 学习程序分析和形式验证的基本原理，它们在高 可信软件、代码优化、并行编译等许多方面有广 泛应用 – 学习和讨论各类方法解决的问题、采用的技术、 理论特性、算法等，并说明这些方法之间的关系 和不同。这些方法本身跨越多种程序设计语言特 征
课程简介（程序分析原理） ·什么是程序分析 一种静态（如编译时)的技术，用于预测程序运 行时动态布局或行为的一种安全（忠实于语义) 且有效（所需时空少）的近似 程序分析的应用 编译时的代码优化， 以避免冗余计算 公共子表达式删除、无用赋值删除、彳 循环优化 一些静态分析工具，用于分析所关心的程序性质 程序切片工具、安全性 -程序验证
课 程 简 介（程序分析原理） • 什么是程序分析 – 一种静态（如编译时）的技术，用于预测程序运 行时动态布局或行为的一种安全（忠实于语义） 且有效（所需时空少）的近似 • 程序分析的应用 – 编译时的代码优化，以避免冗余计算 公共子表达式删除、无用赋值删除、循环优化 – 一些静态分析工具，用于分析所关心的程序性质 程序切片工具、安全性 – 程序验证
课程简介（程序分析原理） 集中在四种主要程序分析方式上 数据流分析(data flow analysis) 基于约束的分析(constraint based analysis) 抽象解释(abstract interpretation) 类型和结果系统(type and effect system) 对每种方式 一描述主要原理，而不是技术的详细介绍 怎样用到更复杂编程语言的分析
课 程 简 介（程序分析原理） • 集中在四种主要程序分析方式上 – 数据流分析(data flow analysis) – 基于约束的分析(constraint based analysis) – 抽象解释(abstract interpretation) – 类型和结果系统(type and effect system) • 对每种方式 – 描述主要原理，而不是技术的详细介绍 – 怎样用到更复杂编程语言的分析
课程简介（模型检测） ·什么是模型检测 验证系统满足性质·( 中)的方法。它操 作在系统的模型 (语义)上，而不是在系统的 描述（语法)上 模型检测的应用 常用于硬件和通信协议的验证中 模型检测方法已经在工业界逐步得到应用，并且 有一些较好的工具
课 程 简 介（模型检测） • 什么是模型检测 – 验证系统 满足性质 （ ）的方法。它操 作在系统的模型 （语义）上，而不是在系统的 描述（语法）上 • 模型检测的应用 – 常用于硬件和通信协议的验证中 – 模型检测方法已经在工业界逐步得到应用，并且 有一些较好的工具
课程简介（模型检测) 集中在采用下面两种逻辑的方法上 线性时态逻辑：时间是线性的逻辑 计算树逻辑：时间可以分支的逻辑 (时态逻辑：公式的真假不是静态的) 模型检测的大体步骤 由用户描述的一个模型开始 -判断用户所断言的假设在模型中是否有效 若无效，则产生由执行轨迹构成的反例
课 程 简 介（模型检测） • 集中在采用下面两种逻辑的方法上 – 线性时态逻辑：时间是线性的逻辑 – 计算树逻辑：时间可以分支的逻辑 （时态逻辑：公式的真假不是静态的） • 模型检测的大体步骤 – 由用户描述的一个模型开始 – 判断用户所断言的假设在模型中是否有效 – 若无效，则产生由执行轨迹构成的反例
课程简介（程序验证） ·什么是程序验证 将基于逻辑证明的方法用于程序性质的证明 1、系统的描述是适当逻辑中的一组公式 2、待证性质的规范是另一个公式中 3、验证就是通过该逻辑来证明工 程序验证的应用 -对安全攸关的程序， 验证所关心的性质 软件的机械验证将改进软件的生产率、效率、 reliability
课 程 简 介（程序验证） • 什么是程序验证 – 将基于逻辑证明的方法用于程序性质的证明 1、系统的描述是适当逻辑中的一组公式 2、待证性质的规范是另一个公式 3、验证就是通过该逻辑来证明 • 程序验证的应用 – 对安全攸关的程序，验证所关心的性质 – 软件的机械验证将改进软件的生产率、效率、 reliability