| 摘要 | 第1-6页 |
| ABSTRACT | 第6-8页 |
| 目录 | 第8-10页 |
| 表格 | 第10-11页 |
| 插图 | 第11-12页 |
| 第1章 绪论 | 第12-23页 |
| ·研究背景 | 第12-15页 |
| ·高可信软件 | 第12页 |
| ·程序验证 | 第12-13页 |
| ·验证编译器 | 第13-14页 |
| ·自动定理证明器 | 第14页 |
| ·Coq | 第14-15页 |
| ·研究现状 | 第15-20页 |
| ·程序验证的相关研究 | 第15-18页 |
| ·自动定理证明技术的相关研究 | 第18-20页 |
| ·本文概述 | 第20-23页 |
| ·研究工作 | 第20-21页 |
| ·本文贡献 | 第21-22页 |
| ·章节安排 | 第22-23页 |
| 第2章 出具证明编译器CComp | 第23-32页 |
| ·源程序 | 第24-29页 |
| ·Clike 语言简介 | 第24-26页 |
| ·断言语言 | 第26-28页 |
| ·源程序示例 | 第28-29页 |
| ·源级验证系统 | 第29-31页 |
| ·自动定理证明器 | 第29-31页 |
| ·目标级验证系统 | 第31页 |
| ·本章小结 | 第31-32页 |
| 第3章 线性整数定理证明器 | 第32-41页 |
| ·线性整数命题分解 | 第33页 |
| ·线性整数表达式规范化 | 第33-34页 |
| ·基于Simplex 算法的决策过程 | 第34-37页 |
| ·线性整数表达式处理 | 第37-38页 |
| ·证明的生成 | 第38-40页 |
| ·本章小结 | 第40-41页 |
| 第4章 证明的管理和构造 | 第41-52页 |
| ·Coq 的证明项 | 第41-42页 |
| ·表示证明项的数据结构 | 第42-44页 |
| ·证明库和证明信息的保存 | 第44-46页 |
| ·证明项的生成 | 第46-51页 |
| ·本章小结 | 第51-52页 |
| 第5章 实验评测 | 第52-56页 |
| ·我们的线性整数定理证明器与Omega 的比较 | 第52-53页 |
| ·出具证明编译器CComp 中线性整数定理证明器的测试 | 第53-54页 |
| ·实验结果总结 | 第54-56页 |
| 第6章 结束语 | 第56-59页 |
| ·论文工作总结 | 第56-57页 |
| ·进一步的工作 | 第57-59页 |
| 参考文献 | 第59-64页 |
| 附录 验证条件的数据结构定义 | 第64-66页 |
| 致谢 | 第66-67页 |
| 在读期间发表的学术论文与取得的研究成果 | 第67页 |