指针逻辑的扩展与应用
| 摘要 | 第1-7页 |
| Abstract | 第7-13页 |
| 第1章 绪论 | 第13-31页 |
| ·指针程序验证的相关研究 | 第14-26页 |
| ·Hoare逻辑 | 第14-17页 |
| ·分离逻辑 | 第17-21页 |
| ·无存储语义方法 | 第21-24页 |
| ·指针逻辑 | 第24-26页 |
| ·存在的问题和发展方向 | 第26-27页 |
| ·本文概述 | 第27-31页 |
| ·研究内容和主要贡献 | 第27-30页 |
| ·章节安排 | 第30-31页 |
| 第2章 指针逻辑 | 第31-57页 |
| ·MiniPointerC | 第31-35页 |
| ·语法 | 第31-33页 |
| ·操作语义 | 第33-35页 |
| ·无存储抽象模型 | 第35-43页 |
| ·访问路径和别名 | 第35-39页 |
| ·内存状态 | 第39-43页 |
| ·指针逻辑 | 第43-54页 |
| ·断言语言 | 第43-46页 |
| ·指针逻辑规则 | 第46-53页 |
| ·保证基本安全性质 | 第53-54页 |
| ·本章小结 | 第54-57页 |
| ·相关工作 | 第54-55页 |
| ·本章小结 | 第55-57页 |
| 第3章 指针逻辑扩展 | 第57-75页 |
| ·e-PointerC语言 | 第57-59页 |
| ·断言语言扩展 | 第59-60页 |
| ·模块化推理 | 第60-65页 |
| ·对象可达性 | 第61-62页 |
| ·推理规则 | 第62-63页 |
| ·实例研究 | 第63-65页 |
| ·支持指针算术的指针逻辑 | 第65-70页 |
| ·推理规则 | 第65-69页 |
| ·实例研究 | 第69-70页 |
| ·带标签的指针逻辑 | 第70-74页 |
| ·推理规则 | 第71-72页 |
| ·实例研究 | 第72-74页 |
| ·本章小结 | 第74-75页 |
| 第4章 指针逻辑验证系统的实现与应用 | 第75-95页 |
| ·指针逻辑规则的实现 | 第75-80页 |
| ·核心算法 | 第76-80页 |
| ·展开机制 | 第80-84页 |
| ·展开归纳谓词 | 第81-83页 |
| ·展开描述性谓词 | 第83-84页 |
| ·Schorr-Waite树遍历算法的自动验证 | 第84-90页 |
| ·算法源代码 | 第85-87页 |
| ·规范 | 第87-89页 |
| ·验证 | 第89-90页 |
| ·实现与实验评估 | 第90-92页 |
| ·本章小结 | 第92-95页 |
| ·相关工作 | 第92-93页 |
| ·本章小结 | 第93-95页 |
| 第5章 结束语 | 第95-99页 |
| ·论文工作总结 | 第95-97页 |
| ·进一步的工作 | 第97-99页 |
| 参考文献 | 第99-105页 |
| 致谢 | 第105-107页 |
| 在读期间发表的学术论文与取得的研究成果 | 第107-108页 |
