本书主要介绍4种程序分析方法——数据流分析、基于约束的分析、抽象解释、类型和作用系统。涵盖基本语义属性和高级算法。全书共6章，第1章为概述，第2～5章依次为数据流分析、基于约束的分析、抽象解释、类型和作用系统，第6章为分析算法介绍。本书基本涵盖了程序分析领域的经典方法和技术，配以严谨的形式化系统，思路清晰、逻辑性强，是学习和研究程序分析原理不可多得的经典书籍。
本书既适合作为程序分析相关硕博研究生课程的教材，也适合相关专业研究人员和专业人士阅读。

冀振燕，副教授，博士生导师。CCF理论计算机专委会委员。1999年7月于中国科学院软件研究所取得博士学位；1999年11月至2000年6月在挪威科技大学作博士后；2000年7月至2008年9月在瑞典Mid-Sweden大学任教；2008年10月至2009年3月在北京工业大学软件学院工作；2009年4月至今在北京交通大学软件学院工作。参与国家级、教育部lBM精品课程“软件系统分析与设计技术”的建设，参与国家级、北京市级教学团队的建设。研究方向：人工智能、计算机视觉、软件服务工程、分布式系统等。承担了多项国家级、省部级科研项目以及企业项目，目前已在国内外知名期刊会议发表论文数十篇，出版书籍多部。

第1章 概述
1.1 什么是程序分析
1.2 设置场景
1.3 数据流分析
1.3.1 等式方法
1.3.2 基于约束的方法
1.4 基于约束的分析
1.5 抽象解释
1.6 类型和作用系统
1.6.1 注释类型系统
1.6.2 作用系统
1.7 算法
1.8 程序转换
结束语
迷你项目
练习
第2章 数据流分析
2.1 过程内数据流分析
2.1.1 可用表达式分析
2.1.2 到达定值分析
2.1.3 很忙的表达式分析
2.1.4 活跃变量分析
2.1.5 派生数据流信息
2.2 理论性质
2.2.1 结构作语义
2.2.2 活跃变量分析的正确性
2.3 单调框架
2.3.1 基本定义
2.3.2 案例回顾
2.3.3 一个不可分配的例子
2.4 等式系统的求解
2.4.1 MFP解
2.4.2 MOP解
2.5 过程间分析
2.5.1 结构作语义
2.5.2 过程内分析与过程间分析
2.5.3 显式使用上下文
2.5.4 调用字符串作为上下文
2.5.5 假设集作为上下文
2.5.6 流敏感与流不敏感
2.6 形状分析
2.6.1 结构作语义
2.6.2 形状图
2.6.3 分析的描述
结束语
迷你项目
练习
第3章 基于约束的分析
3.1 抽象0-CFA分析
3.1.1 分析的描述
3.1.2 分析的明确定义
3.2 理论性质
3.2.1 结构作语义
3.2.2 语义正确性
3.2.3 解的存在性
3.2.4 余归纳和归纳的比较
3.3 语法引导的0-CFA分析
3.3.1 语法引导的规范
3.3.2 解的保持
3.4 基于约束的0-CFA分析
3.4.1 解的保持
3.4.2 约束的求解
3.5 添加数据流分析
3.5.1 抽象值为幂集
3.5.2 抽象值为完全格
3.6 添加上下文信息
3.6.1 均匀k-CFA分析
3.6.2 笛卡儿积算法
结束语
迷你项目
练习
第4章 抽象解释
4.1 一种普通的正确性定义
4.1.1 正确性关系
4.1.2 表示函数
4.1.3 一个较小的扩展
4.2 不动点的近似
4.2.1 加宽算子
4.2.2 变窄算子
4.3 Galois连接
4.3.1 Galois连接的性质
4.3.2 Galois插入
4.4 Galois连接的系统的设计方法
4.4.1 组件上的组合
4.4.2 其他组合方式
4.5 衍生的作
4.5.1 沿着抽象化函数衍生
4.5.2 数据流分析中的应用
4.5.3 沿着具体化函数衍生
结束语
迷你项目
练习
第5章 类型和作用系统
5.1 控制流分析
5.1.1 底层类型系统
5.1.2 基于类型的分析
5.2 理论性质
5.2.1 自然语义
5.2.2 语义正确性
5.2.3 解的存在性
5.3 类型推导算法
5.3.1 一个底层类型系统的算法
5.3.2 一个控制流分析的算法
5.3.3 语法可靠性和完备性
5.3.4 解的存在性
5.4 作用
5.4.1 副作用分析
5.4.2 异常分析
5.4.3 区域推导
5.5 行为
5.5.1 通信分析
结束语
迷你项目
练习
第6章 算法
6.1 工作列表算法
6.1.1 工作列表算法的结构
6.1.2 LIFO和FIFO迭代
6.2 逆后序迭代
6.2.1 循环算法
6.3 在强分量里迭代
结束语
迷你项目
练习
附录A 偏序集合
附录B 归纳和余归纳
附录C 图和正则表达式
参考文献
符号索引
术语索引