| 摘要 | 第5-6页 |
| ABSTRACT | 第6页 |
| 缩略语对照表 | 第9-12页 |
| 第一章 绪论 | 第12-16页 |
| 1.1 研究背景和意义 | 第12-13页 |
| 1.2 模型检测的历史发展和现状 | 第13-14页 |
| 1.3 论文的主要工作和目标 | 第14页 |
| 1.4 论文结构 | 第14-16页 |
| 第二章 相关基础理论和工具 | 第16-26页 |
| 2.1 模型检测 | 第16-17页 |
| 2.1.1 模型检测的基本思想和流程 | 第16页 |
| 2.1.2 时序逻辑 | 第16-17页 |
| 2.2 模型检测中的状态空间爆炸问题及优化技术 | 第17-21页 |
| 2.2.1 抽象技术 | 第18-20页 |
| 2.2.2 其他优化技术 | 第20-21页 |
| 2.3 相关工具 | 第21-24页 |
| 2.3.1 CIL | 第21-22页 |
| 2.3.2 CPAChecker | 第22-24页 |
| 2.4 本章总结 | 第24-26页 |
| 第三章 以CEGAR为基础的C程序PPTL模型检测 | 第26-42页 |
| 3.1 性质的生成 | 第27-32页 |
| 3.1.1 命题和性质的基本形式 | 第27-28页 |
| 3.1.2 命题的形式转化 | 第28-30页 |
| 3.1.3 PPTL的NF范式 | 第30-32页 |
| 3.2 生成抽象状态的过程 | 第32-33页 |
| 3.3 反例路径的形成和细化过程 | 第33-36页 |
| 3.3.1 后继状态的计算 | 第33-35页 |
| 3.3.2 反例路径的判断和细化 | 第35-36页 |
| 3.4 循环检测加速 | 第36-40页 |
| 3.4.1 循环的分类 | 第36页 |
| 3.4.2 简单循环和复杂循环的处理 | 第36-40页 |
| 3.4.3 循环的嵌套分析 | 第40页 |
| 3.5 本章小结 | 第40-42页 |
| 第四章 数组越界自动检测 | 第42-52页 |
| 4.1 数组边界信息的提取 | 第42-46页 |
| 4.2 计算ARG状态的命题的真伪 | 第46-50页 |
| 4.3 循环的改进处理 | 第50-51页 |
| 4.4 本章小结 | 第51-52页 |
| 第五章 实验结果分析 | 第52-56页 |
| 5.1 算法的实验效果 | 第52-55页 |
| 5.2 本章小结 | 第55-56页 |
| 第六章 总结与展望 | 第56-58页 |
| 参考文献 | 第58-62页 |
| 致谢 | 第62-64页 |
| 作者简介 | 第64-65页 |