文摘
英文文摘
声明
第1章绪论
1.1指针程序验证的相关研究
1.1.1 Hoare逻辑
1.1.2分离逻辑
1.1.3无存储语义方法
1.1.4指针逻辑
1.2存在的问题和发展方向
1.3本文概述
1.3.1研究内容和主要贡献
1.3.2章节安排
第2章指针逻辑
2.1 MiniPointerC
2.1.1语法
2.1.2操作语义
2.2无存储抽象模型
2.2.1访问路径和别名
2.2.2内存状态
2.3指针逻辑
2.3.1断言语言
2.3.2指针逻辑规则
2.3.3保证基本安全性质
2.4本章小结
2.4.1相关工作
2.4.2本章小结
第3章指针逻辑扩展
3.1 e-PointerC语言
3.2断言语言扩展
3.3模块化推理
3.3.1对象可达性
3.3.2推理规则
3.3.3实例研究
3.4支持指针算术的指针逻辑
3.4.1推理规则
3.4.2实例研究
3.5带标签的指针逻辑
3.5.1推理规则
3.5.2实例研究
3.6本章小结
第4章指针逻辑验证系统的实现与应用
4.1指针逻辑规则的实现
4.2展开机制
4.2.1展开归纳谓词
4.2.2展开描述性谓词
4.3 Schorr-Waite树遍历算法的自动验证
4.3.1算法源代码
4.3.2规范
4.3.3验证
4.4实现与实验评估
4.5本章小结
4.5.1相关工作
4.5.2本章小结
第5章结束语
5.1论文工作总结
5.2进一步的工作
参考文献
致谢
在读期间发表的学术论文与取得的研究成果