| 摘要 | 第5-6页 |
| ABSTRACT | 第6-7页 |
| 第1章 绪论 | 第14-19页 |
| 1.1 研究背景 | 第14-16页 |
| 1.1.1 高可信软件 | 第14页 |
| 1.1.2 软件测试和形式验证 | 第14-15页 |
| 1.1.3 自动定理证明和Z3 | 第15页 |
| 1.1.4 相关工作比较 | 第15-16页 |
| 1.2 本文概述 | 第16-19页 |
| 1.2.1 研究工作 | 第16-17页 |
| 1.2.2 主要贡献 | 第17页 |
| 1.2.3 章节安排 | 第17-19页 |
| 第2章 验证条件证明器的项目背景和设计概要 | 第19-25页 |
| 2.1 安全C语言验证系统 | 第19-22页 |
| 2.1.1 安全C语言 | 第19页 |
| 2.1.2 安全C语言验证系统框架 | 第19-21页 |
| 2.1.3 安全C语言验证条件 | 第21-22页 |
| 2.2 安全C语言验证条件证明器 | 第22-24页 |
| 2.2.1 验证条件证明器概要 | 第22-23页 |
| 2.2.2 验证条件证明器架构和接口 | 第23-24页 |
| 2.3 本章小结 | 第24-25页 |
| 第3章 验证条件翻译方案的设计和实现 | 第25-44页 |
| 3.1 验证条件的翻译流程 | 第25-32页 |
| 3.1.1 翻译的源语言SCSL及其中间表示形式 | 第25-29页 |
| 3.1.2 翻译目标语言Z3 SMT2 | 第29页 |
| 3.1.3 验证条件的翻译框架设计和实现 | 第29-32页 |
| 3.2 SCSL断言语法树中表达式的翻译 | 第32-41页 |
| 3.2.1 各类型的表达式翻译策略 | 第32-37页 |
| 3.2.2 几类原SCSL中特有类型的Z3 SMT2构造和翻译策略 | 第37-40页 |
| 3.2.3 逻辑对象和附加断言翻译策略 | 第40-41页 |
| 3.3 安全C程序验证中Z3的不足之处的简要分析 | 第41-43页 |
| 3.3.1 安全C程序验证中Z3的表达能力不足分析 | 第41-42页 |
| 3.3.2 安全C程序验证中Z3的证明能力不足分析 | 第42-43页 |
| 3.4 本章小结 | 第43-44页 |
| 第4章 逻辑字符串类型及其翻译方案的设计与实现 | 第44-58页 |
| 4.1 SCSL逻辑字符串类型及操作集 | 第44-49页 |
| 4.1.1 SCSL逻辑字符串类型 | 第44-45页 |
| 4.1.2 SCSL字符串类型的操作集 | 第45-49页 |
| 4.2 SCSL字符串类型的程序标注实例 | 第49-50页 |
| 4.3 SCSL逻辑字符串类型在Z3上的实现方案 | 第50-57页 |
| 4.3.1 Z3 SMT2字符串类型 | 第51页 |
| 4.3.2 Z3 SMT2字符串类型的操作集 | 第51-57页 |
| 4.4 本章小结 | 第57-58页 |
| 第5章 引理证明框架设计和实现 | 第58-67页 |
| 5.1 归纳谓词在程序验证中的必要性 | 第58-59页 |
| 5.2 归纳引理在程序验证中的必要性 | 第59-61页 |
| 5.3 谓词和引理的序关系 | 第61-62页 |
| 5.3.1 谓词的序关系概念和定义 | 第61-62页 |
| 5.3.2 引理的序关系概念和定义 | 第62页 |
| 5.4 引理证明框架和算法细节 | 第62-66页 |
| 5.4.1 引理证明算法框架简介 | 第63页 |
| 5.4.2 引理的分类 | 第63页 |
| 5.4.3 引理证明的依赖分析 | 第63页 |
| 5.4.4 单条引理的归纳证明过程 | 第63-65页 |
| 5.4.5 引理证明完整算法过程 | 第65-66页 |
| 5.5 本章小结 | 第66-67页 |
| 第6章 实例分析和测试结果 | 第67-75页 |
| 6.1 字符串类型的翻译实例 | 第67-71页 |
| 6.2 引理正确性的证明实例 | 第71-74页 |
| 6.3 本章小结 | 第74-75页 |
| 第7章 总结及展望 | 第75-77页 |
| 7.1 总结和相关工作对比 | 第75-76页 |
| 7.2 不足和进一步工作展望 | 第76-77页 |
| 参考文献 | 第77-80页 |
| 致谢 | 第80-82页 |
| 在读期间发表的学术论文与取得的其他研究成果 | 第82页 |
