| 第1章 引言 | 第1-10页 |
| ·软件测试 | 第6-7页 |
| ·静态软件测试 | 第7-8页 |
| ·论文的内容以及组织 | 第8-10页 |
| ·作者的主要研究工作 | 第8-9页 |
| ·论文的组织 | 第9-10页 |
| 第2章 静态测试的研究现状 | 第10-18页 |
| ·传统的程序分析 | 第10-11页 |
| ·静态测试中的程序分析 | 第11-14页 |
| ·符号执行 | 第12页 |
| ·定理证明 | 第12-13页 |
| ·类型推导(type inference) | 第13页 |
| ·抽象解释(abstract interpretation) | 第13页 |
| ·基于规则的静态测试 | 第13-14页 |
| ·模型检测 | 第14页 |
| ·目前的一些静态分析测试项目 | 第14-16页 |
| ·PREfix | 第14-15页 |
| ·ESC | 第15页 |
| ·Metal & ESP | 第15页 |
| ·BANE | 第15-16页 |
| ·SLAM | 第16页 |
| ·Lint | 第16页 |
| ·Cyclone & Vault | 第16页 |
| ·小结 | 第16-18页 |
| 第3章 路径可行性分析工具PAT | 第18-24页 |
| ·PAT的输入 | 第18-19页 |
| ·路径的符号执行 | 第19-20页 |
| ·利用约束求解工具Bonus对约束集合求解 | 第20-21页 |
| ·小结 | 第21-24页 |
| 第4章 包含指针的程序路径的分析 | 第24-44页 |
| ·背景 | 第24页 |
| ·变量关系图 | 第24-28页 |
| ·变量关系图的定义 | 第25-26页 |
| ·基本数据类型的表示 | 第26-27页 |
| ·结构类型变量的表示 | 第27-28页 |
| ·变量关系图的构造和调整 | 第28-32页 |
| ·变量关系图的构造 | 第28页 |
| ·变量在关系图中对应的结点的定位 | 第28-29页 |
| ·赋值动作 | 第29页 |
| ·存储的分配和释放 | 第29-30页 |
| ·过程调用 | 第30-32页 |
| ·利用变量关系图根据规约检测程序 | 第32-41页 |
| ·悬空指针引用检测 | 第32页 |
| ·变量初始化检测 | 第32页 |
| ·程序存储泄漏检测 | 第32-35页 |
| ·变量关系图与符号执行的结合 | 第35-41页 |
| ·工具的实现 | 第41-42页 |
| ·小结 | 第42-44页 |
| 第5章 PAT中的规约及其翻译 | 第44-52页 |
| ·形式规约 | 第44-47页 |
| ·VDM | 第44页 |
| ·B | 第44-45页 |
| ·Z | 第45页 |
| ·CLEAR | 第45页 |
| ·SDL、Estelle及LOTOS | 第45-46页 |
| ·Larch & JML | 第46页 |
| ·断言 | 第46-47页 |
| ·PAT的规约语言的设计 | 第47-50页 |
| ·形式规约的翻译 | 第50-51页 |
| ·小结 | 第51-52页 |
| 第6章 总结 | 第52-54页 |
| ·工作的总结和讨论 | 第52-53页 |
| ·进一步的工作 | 第53-54页 |
| 附录1 PAT接受的程序路径的BNF文法 | 第54-56页 |
| 附录2 PAT中使用的规约语言的BNF文法 | 第56-58页 |
| 参考文献 | 第58-62页 |
| 发表文章目录 | 第62-64页 |
| 致谢 | 第64页 |