安全C语言验证器的形状系统的扩展设计与实现
摘要 | 第5-6页 |
ABSTRACT | 第6-7页 |
第1章 绪论 | 第13-19页 |
1.1 研究背景 | 第13-14页 |
1.1.1 高可信软件 | 第13页 |
1.1.2 软件测试和形式验证 | 第13-14页 |
1.2 本文概述 | 第14-16页 |
1.2.1 本文工作 | 第14-15页 |
1.2.2 主要贡献 | 第15-16页 |
1.3 相关工作 | 第16页 |
1.4 本文章节安排 | 第16-19页 |
第2章 安全C语言验证器及形状系统简介 | 第19-27页 |
2.1 安全C语言验证器简介 | 第19-21页 |
2.2 形状系统简介 | 第21-24页 |
2.3 示例程序的演算分析 | 第24-26页 |
2.4 本章小结 | 第26-27页 |
第3章 形状系统演算的扩展实现 | 第27-43页 |
3.1 角标指针访问路径的节点定位演算 | 第27-34页 |
3.1.1 C风格指针访问路径的局限性 | 第27-28页 |
3.1.2 角标指针访问路径的概述 | 第28-29页 |
3.1.3 角标指针访问路径的节点定位演算详述 | 第29-34页 |
3.2 函数调用演算 | 第34-41页 |
3.2.1 函数调用演算概述 | 第34-36页 |
3.2.2 函数调用演算的窗口获取算法 | 第36-38页 |
3.2.3 函数调用演算的窗口合并算法 | 第38-41页 |
3.3 本章小结 | 第41-43页 |
第4章 形状系统的形状图构造方法改进 | 第43-55页 |
4.1 形状图精确构造方法 | 第43-51页 |
4.1.1 形状图精确构造方法概述 | 第43-44页 |
4.1.2 内置形状谓词阐述 | 第44-46页 |
4.1.3 形状图精确构造方法的操作语义 | 第46-49页 |
4.1.4 形状图精确构造方法的算法描述 | 第49-51页 |
4.2 自定义谓词的推断方法 | 第51-54页 |
4.2.1 自定义谓词推断方法概述 | 第51页 |
4.2.2 自定义谓词推断方法的算法描述 | 第51-54页 |
4.3 本章小结 | 第54-55页 |
第5章 形状系统的形状检查方法扩展 | 第55-67页 |
5.1 指针域标注概述 | 第55-56页 |
5.2 形状检查方法概述 | 第56-59页 |
5.2.1 形状级别概述 | 第56-57页 |
5.2.2 显式形状检查与隐式形状检查 | 第57-58页 |
5.2.3 形状检查方法的总体流程 | 第58-59页 |
5.3 形状检查方法三阶段处理详述 | 第59-66页 |
5.3.1 形状分割 | 第59-61页 |
5.3.2 形状分析 | 第61-64页 |
5.3.3 形状推断 | 第64-66页 |
5.4 本章小结 | 第66-67页 |
第6章 实验结果与实例分析 | 第67-75页 |
6.1 形状检查的实验结果及实例分析 | 第67-70页 |
6.1.1 形状检查的实验结果 | 第67-68页 |
6.1.2 形状检查的实例分析 | 第68-70页 |
6.2 形状系统的综合实验结果及实例解释 | 第70-73页 |
6.2.1 形状系统综合实验结果 | 第70-71页 |
6.2.2 综合实验的实例分析 | 第71-73页 |
6.3 本章小结 | 第73-75页 |
第7章 总结与进一步工作 | 第75-77页 |
7.1 工作总结 | 第75页 |
7.2 进一步工作 | 第75-77页 |
参考文献 | 第77-81页 |
附录A 内置形状谓词产生的形状图 | 第81-83页 |
致谢 | 第83-85页 |
在读期间发表的学术论文与取得的研究成果 | 第85页 |