指针逻辑的扩展与应用
摘要 | 第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页 |