| 摘要 | 第1-7页 |
| Abstract | 第7-13页 |
| 第一章 绪论 | 第13-21页 |
| ·研究背景及相关工作 | 第13-16页 |
| ·同步机制 | 第14页 |
| ·并行程序正确性验证 | 第14-16页 |
| ·存在的问题 | 第16-17页 |
| ·本文的主要工作及贡献 | 第17-18页 |
| ·章节安排 | 第18-21页 |
| 第二章 相关理论与技术基础 | 第21-47页 |
| ·程序正确性检测方法 | 第21-23页 |
| ·携带证明的代码(PCC) | 第23-24页 |
| ·同步技术基础 | 第24-31页 |
| ·基本概念 | 第24-26页 |
| ·各种同步机制的实现 | 第26-31页 |
| ·并行程序验证技术 | 第31-43页 |
| ·不变式证明技术 | 第33-35页 |
| ·Rely-Guarantee推理 | 第35-37页 |
| ·分离逻辑 | 第37-39页 |
| ·并发分离逻辑(CSL) | 第39-40页 |
| ·结合R-G推理和分离逻辑(RGsep和SAGL) | 第40-41页 |
| ·局部R-G推理(LRG) | 第41-42页 |
| ·分析比较 | 第42-43页 |
| ·CCAP验证框架 | 第43-46页 |
| ·元逻辑 | 第43-44页 |
| ·抽象机器 | 第44页 |
| ·目标程序性质的证明框架 | 第44-45页 |
| ·验证框架构造步骤 | 第45-46页 |
| ·本章小结 | 第46-47页 |
| 第三章 使用读写锁的并行程序验证 | 第47-73页 |
| ·问题描述 | 第47-48页 |
| ·CSL的局限性 | 第47-48页 |
| ·所有权转移推理方法 | 第48-50页 |
| ·抽象机器 | 第50-52页 |
| ·扩展并发分离逻辑 | 第52-57页 |
| ·目标程序性质的证明框架 | 第57-68页 |
| ·断言语言和规范语言的语法 | 第57-60页 |
| ·推理规则 | 第60-63页 |
| ·可靠性定理 | 第63-68页 |
| ·目标代码验证举例 | 第68-70页 |
| ·本章小结 | 第70-73页 |
| 第四章 使用可重入锁的并行程序验证 | 第73-87页 |
| ·问题描述 | 第73-75页 |
| ·抽象机器 | 第75-77页 |
| ·目标程序性质的证明框架 | 第77-83页 |
| ·断言语言和规范语言的语法 | 第77-80页 |
| ·推理规则 | 第80-83页 |
| ·可靠性定理 | 第83页 |
| ·目标代码验证举例 | 第83-85页 |
| ·本章小结 | 第85-87页 |
| 第五章 验证框架的Coq实现 | 第87-99页 |
| ·抽象机器在Coq中的描述 | 第87-92页 |
| ·机器语法定义 | 第87-90页 |
| ·机器操作语义定义 | 第90-92页 |
| ·程序规范在Coq中的描述 | 第92页 |
| ·强弱分离在Coq中的描述 | 第92-93页 |
| ·推理规则在Coq中的描述 | 第93-95页 |
| ·框架可靠性证明 | 第95-97页 |
| ·本章小结 | 第97-99页 |
| 第六章 使用混合同步控制机制的并行程序验证 | 第99-109页 |
| ·问题描述 | 第99-101页 |
| ·支持可逆代码块的并行语言 | 第101-105页 |
| ·可逆代码块"rev{C}" | 第102-103页 |
| ·语法 | 第103-104页 |
| ·程序实例 | 第104-105页 |
| ·验证可逆代码块中的问题 | 第105-107页 |
| ·操作语义 | 第105-106页 |
| ·推理规则 | 第106-107页 |
| ·本章小结 | 第107-109页 |
| 第七章 结束语 | 第109-111页 |
| ·论文工作总结 | 第109页 |
| ·进一步的工作 | 第109-111页 |
| 参考文献 | 第111-121页 |
| 致谢 | 第121-123页 |
| 在读期间发表的学术论文与取得的研究成果 | 第123-124页 |