| 摘要 | 第8-9页 |
| ABSTRACT | 第9页 |
| 第1章 绪论 | 第10-16页 |
| 1.1 研究背景 | 第10-11页 |
| 1.2 有研究成果 | 第11-14页 |
| 1.2.1 国内外研究现状 | 第11-13页 |
| 1.2.2 发展趋势 | 第13-14页 |
| 1.3 课题目标与研究内容 | 第14页 |
| 1.3.1 课题目标 | 第14页 |
| 1.3.2 研究内容 | 第14页 |
| 1.4 论文结构 | 第14-16页 |
| 第2章 数组越界检查相关理论与关键技术 | 第16-23页 |
| 2.1 基于抽象解释的值范围分析 | 第16-19页 |
| 2.1.1 基于Galois连接的抽象解释理论下的程序语义 | 第16-17页 |
| 2.1.2 基于单调数据流的值范围分析 | 第17-19页 |
| 2.2 基于值范围分析的数组越界检查技术 | 第19-23页 |
| 2.2.1 数组越界问题剖析 | 第19-21页 |
| 2.2.2 数组越界检查总体思路 | 第21-23页 |
| 第3章 数组越界检查工具总体框架 | 第23-33页 |
| 3.1 抽象解释器前端Interproc | 第24-30页 |
| 3.1.1 Interproc简介 | 第24页 |
| 3.1.2 Interproc输入—Simple语言介绍 | 第24-29页 |
| 3.1.3 面向数组的Simple语法扩展 | 第29-30页 |
| 3.2 数值抽象域库APRON | 第30-31页 |
| 3.3 不动点求解器模块 | 第31-33页 |
| 3.3.1 循环语句分析过程 | 第32页 |
| 3.3.2 加宽和加宽延迟策略 | 第32-33页 |
| 第4章 面向数组分析的抽象域设计与实现 | 第33-48页 |
| 4.1 基于合并语义的数组抽象域arrayMerge | 第33-42页 |
| 4.1.1 arrayMerge设计思路 | 第33-34页 |
| 4.1.2 arrayMerge实现细节 | 第34-41页 |
| 4.1.3 实例分析 | 第41-42页 |
| 4.2 基于分离语义的数组抽象域arraySmash | 第42-48页 |
| 4.2.1 arraySmash设计思想 | 第42-43页 |
| 4.2.2 arraySmash实现细节 | 第43-46页 |
| 4.2.3 实例分析 | 第46-48页 |
| 第5章 实验结果与分析 | 第48-54页 |
| 第6章 结束语 | 第54-56页 |
| 6.1 本文的主要工作 | 第54-55页 |
| 6.2 下一步工作 | 第55-56页 |
| 参考文献 | 第56-59页 |
| 致谢 | 第59-60页 |
| 学位论文评阅及答辩情况表 | 第60页 |
