用形式化方法构建安全的线程机制
| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 第1章 绪论 | 第8-14页 |
| ·研究背景和意义 | 第8页 |
| ·研究现状 | 第8-10页 |
| ·基于类型系统的并发系统安全研究 | 第9页 |
| ·基于程序验证的并发系统安全研究 | 第9-10页 |
| ·本文工作与贡献 | 第10-12页 |
| ·章节安排 | 第12-14页 |
| 第2章 术语表 | 第14-16页 |
| 第3章 基本设定与主要技术 | 第16-29页 |
| ·归纳构造演算与证明辅助工具 Coq | 第16-18页 |
| ·归纳构造演算 | 第16-17页 |
| ·证明辅助工具Coq | 第17-18页 |
| ·抽象机器模型 | 第18-20页 |
| ·并发代码的推理方法 | 第20-22页 |
| ·假设-保证推理方法 | 第20-21页 |
| ·并发分离逻辑 | 第21-22页 |
| ·基于语法的携带基础证明代码 | 第22-29页 |
| ·携带基础证明代码 | 第22页 |
| ·用语法制导的推理规则描述程序逻辑 | 第22-23页 |
| ·抽象控制栈 | 第23-25页 |
| ·支持假设-保证推理方法 | 第25-26页 |
| ·携带证明代码模块的连接 | 第26-29页 |
| 第4章 一个简单的线程库 | 第29-33页 |
| ·API | 第29-30页 |
| ·线程模型与基本数据结构 | 第30-31页 |
| ·实现简要 | 第31-33页 |
| 第5章 线程库的安全规范与证明 | 第33-39页 |
| ·证明方法 | 第33-34页 |
| ·接口规范 | 第34-35页 |
| ·实现规范 | 第35-36页 |
| ·实现规范的证明 | 第36-37页 |
| ·接口规范的证明 | 第37-39页 |
| 第6章 证明的简化 | 第39-41页 |
| 第7章 实用价值分析 | 第41-45页 |
| ·实用价值 | 第41-42页 |
| ·TCB 范围 | 第42-45页 |
| 第8章 相关工作比较 | 第45-49页 |
| ·Mth | 第45-47页 |
| ·Verisoft XT | 第47-49页 |
| 第9章 结论 | 第49-51页 |
| 参考文献 | 第51-54页 |
| 致谢 | 第54-55页 |
| 在读期间发表的学术论文与取得的其他研究成果 | 第55页 |
