用于指针逻辑的自动定理证明器的设计与实现
| 摘要 | 第1-7页 |
| ABSTRACT | 第7-11页 |
| 第1章 绪论 | 第11-31页 |
| ·背景研究 | 第11-19页 |
| ·形式化方法 | 第11-12页 |
| ·指针程序验证 | 第12-13页 |
| ·定理证明器 | 第13-16页 |
| ·证明检查器 | 第16-17页 |
| ·模型检查 | 第17-19页 |
| ·研究现状 | 第19-27页 |
| ·分离逻辑 | 第19-21页 |
| ·指针断言逻辑 | 第21-23页 |
| ·形状分析 | 第23-24页 |
| ·出具证明编译器 | 第24-27页 |
| ·问题描述 | 第27-28页 |
| ·本文概述 | 第28-31页 |
| ·所做研究 | 第28-29页 |
| ·本文贡献 | 第29-30页 |
| ·章节安排 | 第30-31页 |
| 第2章 指针逻辑 | 第31-43页 |
| ·基本概念 | 第31-32页 |
| ·断言语言 | 第32-40页 |
| ·断言语言设计 | 第33-36页 |
| ·断言演算 | 第36-40页 |
| ·规范语言 | 第40-41页 |
| ·公理和推理规则 | 第41-43页 |
| 第3章 APL自动定理证明器 | 第43-74页 |
| ·APL系统组成 | 第43-45页 |
| ·主函数算法 | 第45-46页 |
| ·验证条件 | 第46-51页 |
| ·验证条件检查器 | 第51-53页 |
| ·指针逻辑决策过程 | 第53-64页 |
| ·公理及推理规则 | 第53-58页 |
| ·决策过程 | 第58-64页 |
| ·整型线性算术决策过程 | 第64-68页 |
| ·Presburger算术 | 第64-65页 |
| ·相关研究 | 第65-66页 |
| ·Cooper算法 | 第66-68页 |
| ·生成证明 | 第68-71页 |
| ·保存证明 | 第71-74页 |
| 第4章 证明检查器 | 第74-78页 |
| ·基本原理 | 第74页 |
| ·证明检查算法 | 第74-77页 |
| ·对比分析 | 第77-78页 |
| 第5章 实验结果 | 第78-80页 |
| ·实验数据 | 第78-79页 |
| ·实验结果分析比较 | 第79-80页 |
| 第6章 结束语 | 第80-82页 |
| ·工作总结 | 第80-81页 |
| ·进一步工作 | 第81-82页 |
| 参考文献 | 第82-88页 |
| 附录1 验证条件的数据结构定义 | 第88-89页 |
| 附录2 Presburger算术的数据结构定义 | 第89-90页 |
| 附录3 APL的文件组成及函数功能说明 | 第90-96页 |
| 致谢 | 第96-98页 |
| 在读期间发表的学术论文与取得的研究成果 | 第98页 |
