目录介绍
第1章程序分析技术1
1.1程序的正确性及其分析1
1.2控制流分析2
1.2.1控制流图2
1.2.2程序依赖图4
1.2.3系统依赖图5
1.3数据流分析6
1.3.1数据流分析概述6
1.3.2可达定义分析8
1.3.3活性变量分析8
本章小结9
第2章符号执行技术10
2.1符号执行概述10
2.2传统符号执行10
2.3混合符号执行13
2.4符号执行技术面临的挑战14
2.4.1内存相关问题15
2.4.2环境相关问题15
2.4.3路径爆炸问题16
2.4.4约束求解问题16
2.5符号执行工具17
2.5.1KLEE17
2.5.2SPF18
2.5.3SAGE19
2.5.4SymCC20
本章小结21
基于程序分析的软件测试与错误定位技术
｜目录｜
第3章软件测试与错误定位技术22
3.1软件测试与错误定位的研究背景23
3.1.1软件测试23
3.1.2软件错误定位24
3.2基于符号执行的软件测试25
3.2.1摘要计算26
3.2.2路径包含与等价分析27
3.2.3约束不充分的符号执行29
3.2.4前置条件与输入特征利用30
3.2.5符号执行状态合并31
3.2.6程序分析及优化技术32
3.2.7目标导向与启发式策略33
3.2.8增量符号执行34
3.2.9并行符号执行36
3.3软件错误定位方法36
3.3.1基于切片的错误定位36
3.3.2基于程序状态的错误定位37
3.3.3基于统计分析的错误定位39
3.3.4基于人工智能的错误定位40
3.3.5演化软件错误定位42
本章小结43
第4章基于执行路径的最弱前置条件计算44
4.1最弱前置条件概述44
4.2最弱前置条件计算45
4.2.1转换实例47
4.2.2关键谓词47
4.3框架设计与实现48
本章小结48
第5章基于后缀路径摘要的符号执行加速49
5.1方法概述49
5.2预备知识50
5.3冗余后缀路径消除52
5.3.1示例程序分析52
5.3.2顶层算法描述56
5.3.3路径后缀描述57
5.3.4冗余路径后缀裁剪58
5.3.5可靠性分析59
5.3.6搜索策略设置61
5.4优化策略61
5.4.1摘要化简62
5.4.2避免冗余最弱前置条件计算64
5.4.3设置冗余路径检测点65
5.4.4控制摘要大小66
5.5方法评估66
5.5.1实验对象及方法67
5.5.2路径裁剪的有效性67
5.5.3路径裁剪的代价71
5.5.4优化策略有效性评估72
本章小结75
第6章基于反馈驱动的增量符号执行76
6.1方法简介76
6.2相关定义77
6.3增量符号执行与反馈驱动分析78
6.3.1总体算法79
6.3.2正向符号执行81
6.3.3后向符号执行81
6.3.4基于ΠΔ的显式路径裁剪83
6.3.5带有路径收缩的隐式路径修剪84
6.3.6例子阐述86
6.3.7讨论88
6.4实验评估89
6.4.1原型工具实现89
6.4.2实验对象和实验设置90
6.4.3SIR实验90
6.4.4GNU Coreutils实验91
6.4.5有效性威胁94
本章小结94
第7章级联式错误定位方法96
7.1方法简介96
7.2级联式错误定位101
7.2.1错误原因的标识102
7.2.2更多可能错误原因的标识104
7.2.3顶层算法的描述106
7.3优化策略107
7.3.1切片处理错误执行路径107
7.3.2指定正确实现函数108
7.3.3简化SMT求解器查询109
7.3.4处理循环与递归109
7.4方法评估111
7.4.1西门子测试程序集评估111
7.4.2Busybox与Coreutils评估115
本章小结121
第8章演化软件错误定位方法122
8.1演化软件错误定位方法概述122
8.2协同分析方法126
8.2.1顶层算法描述126
8.2.2动态分析128
8.2.3计算辅助代码改变块129
8.3示例阐述131
8.3.1演化软件错误定位方法的应用132
8.3.2与相关方法的比较134
8.4实验分析135
8.4.1错误解释的精确性137
8.4.2运行性能的比较138
8.4.3协同分析的有效性139
本章小结141
第9章符号执行指导的并行程序分析142
9.1方法介绍142
9.2方法概述144
9.2.1示例阐述144
9.2.2最大因果关系规约145
9.2.3最大路径因果关系概述147
9.3最大路径因果关系方法150
9.3.1基本定义150
9.3.2最大路径因果关系151
9.3.3基本算法152
9.3.4路径遍历154
9.3.5并行的MPC算法157
9.4方法评估158
9.4.1检测并行程序错误158
9.4.2并发库的评估160
9.4.3与工具Con2Colic的比较161
本章小结163
参 考文献164