基于携带证明的代码的垃圾收集过程验证
| 摘要 | 第1-7页 |
| Abstract | 第7-12页 |
| 第1章 绪论 | 第12-30页 |
| ·垃圾收集技术 | 第13-18页 |
| ·基本概念 | 第13-14页 |
| ·经典垃圾收集算法 | 第14-15页 |
| ·用户程序和垃圾收集器的交互方式 | 第15-17页 |
| ·精确的和保守的垃圾收集 | 第17页 |
| ·垃圾收集的安全性问题 | 第17-18页 |
| ·形式程序验证和携带证明的代码 | 第18-23页 |
| ·经典Hoare逻辑 | 第18-19页 |
| ·携带证明的代码 | 第19-21页 |
| ·基础的携带证明的代码 | 第21-23页 |
| ·相关研究工作 | 第23-27页 |
| ·形式程序验证 | 第23-24页 |
| ·垃圾收集验证 | 第24-26页 |
| ·类型安全的垃圾收集 | 第26-27页 |
| ·本文概述 | 第27-30页 |
| ·主要贡献、技术特点和创新之处 | 第27-29页 |
| ·章节安排 | 第29-30页 |
| 第2章 验证框架 | 第30-49页 |
| ·元逻辑 | 第30-31页 |
| ·抽象机器模型 | 第31-36页 |
| ·讨论 | 第35-36页 |
| ·开放式汇编语言程序推理系统 | 第36-41页 |
| ·推理规则 | 第38-40页 |
| ·可靠性和正确性 | 第40-41页 |
| ·模块化验证栈式控制流程序的推理方法 | 第41-46页 |
| ·验证条件产生器 | 第45-46页 |
| ·分离逻辑风格的代码规范语言 | 第46-49页 |
| 第3章 垃圾收集器验证 | 第49-84页 |
| ·基本假定和相关定义 | 第49-51页 |
| ·停止式标记-清扫垃圾收集器 | 第51-67页 |
| ·原理及算法 | 第51-54页 |
| ·堆数据结构形式定义 | 第54-56页 |
| ·垃圾收集器规范 | 第56-58页 |
| ·构造证明 | 第58-67页 |
| ·Yuasa渐进式垃圾收集器 | 第67-84页 |
| ·交互式的垃圾收集 | 第67-68页 |
| ·原理及算法 | 第68-71页 |
| ·弱三色抽象不变式 | 第71-75页 |
| ·垃圾收集器规范 | 第75-78页 |
| ·构造证明 | 第78-84页 |
| 第4章 验证垃圾收集过程的通用框架 | 第84-97页 |
| ·基于ADT的垃圾收集器接口规范 | 第86-94页 |
| ·抽象存储状态和具体存储状态 | 第87-89页 |
| ·抽象规范和具体规范 | 第89-94页 |
| ·基于抽象接口规范的用户程序验证 | 第94-95页 |
| ·基于抽象接口规范的垃圾收集器验证 | 第95-97页 |
| 第5章 为类型化汇编语言构造验证的垃圾收集过程 | 第97-115页 |
| ·方法概述 | 第97-99页 |
| ·验证垃圾收集器 | 第99-101页 |
| ·基础的类型化汇编语言 | 第101-109页 |
| ·类型定义 | 第102-103页 |
| ·定型规则 | 第103-106页 |
| ·嵌入OCAP_(LITE)框架 | 第106-109页 |
| ·证明垃圾收集器接口规范的一致性 | 第109-112页 |
| ·链接实例 | 第112-115页 |
| 第6章 验证工作的COQ实现 | 第115-129页 |
| ·计算机辅助定理证明工具COQ | 第115-116页 |
| ·验证框架 | 第116-122页 |
| ·验证垃圾收集器 | 第122页 |
| ·验证垃圾收集器和用户程序交互 | 第122-125页 |
| ·类型化汇编语言和验证的垃圾收集 | 第125-127页 |
| ·讨论 | 第127-129页 |
| 第7章 结束语 | 第129-132页 |
| ·文章总结 | 第129-130页 |
| ·对后续研究的展望 | 第130-132页 |
| 参考文献 | 第132-141页 |
| 致谢 | 第141-142页 |
| 在读期间发表的学术论文与取得的研究成果 | 第142页 |
