| 摘要 | 第5-7页 |
| ABSTRACT | 第7-8页 |
| 目录 | 第9-12页 |
| 表格索引 | 第12-13页 |
| 插图索引 | 第13-14页 |
| 算法索引 | 第14-15页 |
| 第一章 简介 | 第15-21页 |
| 1.1 程序的正确性 | 第15页 |
| 1.2 程序正确性证明 | 第15页 |
| 1.3 程序的错误检测 | 第15-17页 |
| 1.3.1 软件测试 | 第16页 |
| 1.3.2 程序分析 | 第16-17页 |
| 1.4 C程序应用的广泛及重要性 | 第17-18页 |
| 1.5 研究内容及贡献 | 第18-19页 |
| 1.5.1 C程序内存泄漏检测 | 第18-19页 |
| 1.5.2 基于函数摘要的多错误检测框架 | 第19页 |
| 1.5.3 面向符号执行的约束求解优化 | 第19页 |
| 1.6 论文组织 | 第19-21页 |
| 第二章 背景介绍 | 第21-31页 |
| 2.1 静态程序分析 | 第21-28页 |
| 2.1.1 控制流图 | 第21页 |
| 2.1.2 数据流分析 | 第21-23页 |
| 2.1.3 符号执行 | 第23-25页 |
| 2.1.4 敏感性分析 | 第25-28页 |
| 2.2 C程序的错误模式 | 第28-29页 |
| 2.2.1 未定义的行为 | 第28-29页 |
| 2.2.2 常见错误模式 | 第29页 |
| 2.3 本章小结 | 第29-31页 |
| 第三章 内存泄漏的自动化检测 | 第31-65页 |
| 3.1 简介 | 第31-33页 |
| 3.2 相关工作 | 第33-38页 |
| 3.3 动机和示例 | 第38-42页 |
| 3.3.1 内存行为 | 第39-41页 |
| 3.3.2 结合路径敏感性的例子 | 第41-42页 |
| 3.4 基于内存状态转移图的内存泄漏检测 | 第42-55页 |
| 3.4.1 算法框架 | 第42页 |
| 3.4.2 过程内分析 | 第42-50页 |
| 3.4.3 过程间分析 | 第50-53页 |
| 3.4.4 示例 | 第53-54页 |
| 3.4.5 本方法的优势及潜在的优化 | 第54-55页 |
| 3.5 具体实现 | 第55-57页 |
| 3.5.1 Clang Static Analyzer概述 | 第55页 |
| 3.5.2 内存泄漏检测器 | 第55-56页 |
| 3.5.3 错误报告生成器 | 第56-57页 |
| 3.6 实验结果 | 第57-64页 |
| 3.6.1 已检测到的内存泄漏 | 第57-60页 |
| 3.6.2 与其他工具的比较 | 第60-64页 |
| 3.7 本章小结 | 第64-65页 |
| 第四章 支持多错误检测的C程序静态分析框架 | 第65-89页 |
| 4.1 简介 | 第65-66页 |
| 4.2 示例 | 第66-67页 |
| 4.3 框架概述 | 第67-69页 |
| 4.3.1 系统架构 | 第67-68页 |
| 4.3.2 错误检测器 | 第68-69页 |
| 4.3.3 框架整体算法 | 第69页 |
| 4.4 基于区域的过程内分析 | 第69-73页 |
| 4.4.1 抽象区域 | 第70-71页 |
| 4.4.2 抽象值 | 第71页 |
| 4.4.3 存储,环境和约束守卫 | 第71-73页 |
| 4.4.4 程序状态 | 第73页 |
| 4.5 过程间符号执行 | 第73-82页 |
| 4.5.1 基于函数摘要的分析 | 第73-81页 |
| 4.5.2 基于内联的过程间分析 | 第81-82页 |
| 4.6 实验结果 | 第82-86页 |
| 4.6.1 实验基准程序 | 第83页 |
| 4.6.2 RQ1：错误检测能力 | 第83-84页 |
| 4.6.3 RQ2：过程间分析的比较 | 第84-85页 |
| 4.6.4 RQ3：与Saturn的比较 | 第85-86页 |
| 4.7 相关工作 | 第86-87页 |
| 4.7.1 基于函数摘要的静态错误检测 | 第86页 |
| 4.7.2 基于内联的程序错误检测 | 第86-87页 |
| 4.7.3 模块化的指针分析 | 第87页 |
| 4.7.4 一般性的模块化分析 | 第87页 |
| 4.8 本章小节 | 第87-89页 |
| 第五章 面向符号执行的轻量级约束求解框架 | 第89-103页 |
| 5.1 简介 | 第89-90页 |
| 5.2 基于赋值重用的约束求解优化 | 第90-96页 |
| 5.2.1 符号执行中的约束求解 | 第90-92页 |
| 5.2.2 全变量赋值重用 | 第92-94页 |
| 5.2.3 复杂约束变量赋值重用 | 第94-95页 |
| 5.2.4 算法复杂度比较 | 第95-96页 |
| 5.3 基于后验证的约束求解优化 | 第96-100页 |
| 5.3.1 约束求解器 | 第97页 |
| 5.3.2 基于后验证的约束求解 | 第97-99页 |
| 5.3.3 实验结果 | 第99-100页 |
| 5.4 相关工作 | 第100-101页 |
| 5.5 本章小结 | 第101-103页 |
| 第六章 结束语 | 第103-105页 |
| 6.1 主要贡献 | 第103页 |
| 6.2 进一步工作 | 第103-105页 |
| 6.2.1 循环的分析 | 第104页 |
| 6.2.2 浮点数的分析 | 第104页 |
| 6.2.3 更多实验以及工具的改进 | 第104-105页 |
| 参考文献 | 第105-109页 |
| 致谢 | 第109-111页 |
| 在读期间发表的学术论文与取得的研究成果 | 第111页 |