| 摘要 | 第1-6页 |
| ABSTRACT | 第6-10页 |
| 第一章 绪论 | 第10-16页 |
| ·研究背景 | 第10-12页 |
| ·已有工作基础 | 第12页 |
| ·本文研究的问题和主要贡献 | 第12-14页 |
| ·章节安排 | 第14-16页 |
| 第二章 技术背景介绍 | 第16-28页 |
| ·程序语言及逻辑 | 第16-25页 |
| ·SCPL语言的语法 | 第16-18页 |
| ·表达式求值的语义 | 第18-19页 |
| ·逻辑断言 | 第19-22页 |
| ·三元组的推理规则 | 第22-24页 |
| ·表达式符号求值的推理规则 | 第24-25页 |
| ·策略编写语言Ltac简介 | 第25-26页 |
| ·本章小结 | 第26-28页 |
| 第三章 分离逻辑断言之间蕴含关系的自动证明策略 | 第28-42页 |
| ·推理断言之间蕴含关系的sep_auto | 第28-38页 |
| ·使断言规范化的sep_normal | 第30-31页 |
| ·消除非纯断言的sep_cancel | 第31-34页 |
| ·sep_auto用到的其他证明策略 | 第34-38页 |
| ·一个使用sep_auto的自动证明实例 | 第38-40页 |
| ·本章小结 | 第40-42页 |
| 第四章 Hoare三元组的自动证明策略 | 第42-60页 |
| ·前向推理三元组的hoare_forward | 第42-52页 |
| ·检查前条件中资源的hoare_unfold | 第44-50页 |
| ·为第一条语句生成后条件的hoare_forward_stmt | 第50-51页 |
| ·表达式符号求值的symbolic_execution | 第51-52页 |
| ·使用hoare_forward自动证明单链表原地逆转的程序 | 第52-55页 |
| ·使用hoare_forward进行交互式证明 | 第55-58页 |
| ·本章小结 | 第58-60页 |
| 第五章 证明策略的Coq实现分析 | 第60-68页 |
| ·证明策略的Coq实现代码统计 | 第60-61页 |
| ·使用证明策略证明的一些程序的统计 | 第61-64页 |
| ·与相关工作的比较 | 第64-66页 |
| ·证明策略的性能分析 | 第66-67页 |
| ·本章小结 | 第67-68页 |
| 第六章 结束语 | 第68-70页 |
| ·论文总结 | 第68页 |
| ·进一步工作 | 第68-70页 |
| 参考文献 | 第70-72页 |
| 致谢 | 第72-74页 |
| 在读期间发表的学术论文与取得的研究成果 | 第74页 |
