面向多核处理器的低级并行程序验证
| 摘要 | 第1-4页 |
| ABSTRACT | 第4-8页 |
| 第1章 引言 | 第8-12页 |
| ·背景简介 | 第8-9页 |
| ·研究目的与内容 | 第9-10页 |
| ·论文结构 | 第10-12页 |
| 第2章 验证编译器 | 第12-24页 |
| ·受信任计算基础（TCB） | 第12-13页 |
| ·规范语言的表达能力 | 第13页 |
| ·带证明代码（PCC） | 第13-15页 |
| ·基础带证明代码（FPCC） | 第15页 |
| ·验证汇编编程（CAP） | 第15-20页 |
| ·Hoare 逻辑 | 第15-16页 |
| ·CAP 验证框架的结构 | 第16-19页 |
| ·基本块为单位的验证方式 | 第19-20页 |
| ·相关项目介绍 | 第20-23页 |
| ·Touchstone 编译器项目 | 第20-21页 |
| ·TAL 项目 | 第21-22页 |
| ·Singularity 项目 | 第22页 |
| ·CCm 项目 | 第22-23页 |
| ·本章小结 | 第23-24页 |
| 第3章 MCAP 验证框架概述 | 第24-34页 |
| ·MCAP 的验证流程及优点 | 第24-26页 |
| ·验证流程 | 第24-25页 |
| ·框架优点 | 第25-26页 |
| ·MCAP 框架结构 | 第26-28页 |
| ·MCAP框架的描述与证明工具Coq | 第28-33页 |
| ·Curry-Howard 同构 | 第28页 |
| ·程序语言GALLINA | 第28-29页 |
| ·命令语言Vernacular | 第29-30页 |
| ·交互式定理证明 | 第30-33页 |
| ·本章小结 | 第33-34页 |
| 第4章 MCAP 验证框架的实现 | 第34-59页 |
| ·MCAP 抽象机器设计 | 第34-42页 |
| ·抽象机设计概述 | 第34-37页 |
| ·双核处理器 | 第34页 |
| ·内核同步 | 第34-35页 |
| ·自旋锁 | 第35页 |
| ·死锁 | 第35-36页 |
| ·内存划分 | 第36-37页 |
| ·抽象机器的形式化定义 | 第37-40页 |
| ·MCAP 抽象机语法 | 第37-38页 |
| ·MCAP 抽象机操作语义 | 第38-40页 |
| ·抽象机器的Coq 描述 | 第40-42页 |
| ·内存拥有权的转移 | 第42-43页 |
| ·程序规范 | 第43-44页 |
| ·推理规则 | 第44-49页 |
| ·推理规则的层次 | 第44-45页 |
| ·推理规则的具体定义 | 第45-49页 |
| ·推理规则的Coq 描述 | 第49页 |
| ·可靠性定理及证明 | 第49-54页 |
| ·可靠性定理 | 第49-50页 |
| ·前进性引理及证明 | 第50-51页 |
| ·保持性引理及证明 | 第51-54页 |
| ·可靠性定理的证明 | 第54页 |
| ·目标代码验证举例 | 第54-58页 |
| ·本章小结 | 第58-59页 |
| 第5章 MCAP 框架的扩展 | 第59-66页 |
| ·真实汇编代码级验证 | 第59-61页 |
| ·自旋锁操作原语的真实汇编表示 | 第59-60页 |
| ·MCAP 推理规则的适用 | 第60-61页 |
| ·函数模块化验证 | 第61-63页 |
| ·MIPS 函数调用实例 | 第61页 |
| ·调用与返回指令推理规则的构造 | 第61-63页 |
| ·Assume-Guarantee技术的引入 | 第63-65页 |
| ·本章小结 | 第65-66页 |
| 第6章 总结与展望 | 第66-68页 |
| ·工作总结 | 第66-67页 |
| ·展望 | 第67-68页 |
| 参考文献 | 第68-71页 |
| 致谢 | 第71-72页 |
| 个人简历、在学期间发表的学术论文与研究成果 | 第72页 |
