| 中文摘要 | 第1-7页 |
| 英文摘要 | 第7-16页 |
| 第一章 绪论 | 第16-38页 |
| §1.1 背景研究 | 第16-19页 |
| §1.1.1 程序性质证明 | 第17页 |
| §1.1.2 软件的可信性 | 第17页 |
| §1.1.3 被信任计算基础 | 第17-18页 |
| §1.1.4 出具证明的编译器 | 第18-19页 |
| §1.2 程序性质证明和出具证明编译的相关研究现状及比较 | 第19-33页 |
| §1.2.1 基于Hoare逻辑推理的程序性质证明研究 | 第19-24页 |
| §1.2.2 基于类型论的程序性质证明方法 | 第24-27页 |
| §1.2.3 结合逻辑方法和类型论方法的研究 | 第27-29页 |
| §1.2.4 验证编译的相关研究 | 第29-33页 |
| §1.3 存在的问题和发展方向 | 第33-34页 |
| §1.4 本文概述 | 第34-38页 |
| §1.4.1 研究工作 | 第34-35页 |
| §1.4.2 特色和贡献 | 第35-36页 |
| §1.4.3 章节安排 | 第36-38页 |
| 第二章 可信程序的设计和证明框架 | 第38-60页 |
| §2.1 程序开发框架描述 | 第38-42页 |
| §2.1.1 传统程序开发框架 | 第38页 |
| §2.1.2 加入了程序验证系统的可信程序开发框架 | 第38-42页 |
| §2.2 源级程序设计和源级验证系统 | 第42-49页 |
| §2.2.1 PointerC语言简介 | 第42-45页 |
| §2.2.2 源级验证系统 | 第45-49页 |
| §2.3 目标级验证系统 | 第49-54页 |
| §2.3.1 FCAP框架 | 第50-52页 |
| §2.3.2 目标级指针逻辑系统 | 第52-54页 |
| §2.4 出具证明编译器 | 第54-56页 |
| §2.4.1 出具证明编译器总体框架 | 第54-56页 |
| §2.4.2 各个模块简介 | 第56页 |
| §2.5 本章小结 | 第56-60页 |
| 第三章 出具证明编译器的前端设计 | 第60-78页 |
| §3.1 前端设计的总体框架 | 第60页 |
| §3.2 主要数据结构 | 第60-67页 |
| §3.2.1 抽象语法树AST | 第61-65页 |
| §3.2.2 符号表TABLE | 第65-67页 |
| §3.3 验证条件生成器的设计 | 第67-76页 |
| §3.3.1 验证条件生成算法 | 第68-70页 |
| §3.3.2 定型规则附加条件的收集 | 第70页 |
| §3.3.3 最弱前条件中的变量替换 | 第70-74页 |
| §3.3.4 验证条件的化简 | 第74-75页 |
| §3.3.5 验证条件生成器对AST的影响 | 第75-76页 |
| §3.4 出具证明特性对编译前端的影响 | 第76-77页 |
| §3.5 本章小结 | 第77-78页 |
| 第四章 出具证明编译器的后端设计 | 第78-100页 |
| §4.1 后端设计的总体框架 | 第78-80页 |
| §4.2 主要数据结构 | 第80-85页 |
| §4.2.1 函数的frame | 第80-81页 |
| §4.2.2 用于代码生成的符号表CodeGen-Table | 第81-82页 |
| §4.2.3 代码抽象表示ASM | 第82-84页 |
| §4.2.4 规范抽象表示ASSERT | 第84-85页 |
| §4.3 代码生成器设计 | 第85-90页 |
| §4.3.1 基本流程 | 第86页 |
| §4.3.2 主要数据结构和约定 | 第86-90页 |
| §4.4 规范翻译器设计 | 第90-98页 |
| §4.4.1 划分基本块 | 第90-91页 |
| §4.4.2 翻译源级规范 | 第91-94页 |
| §4.4.3 形式规范的调整 | 第94-95页 |
| §4.4.4 生成中间规范 | 第95-98页 |
| §4.5 出具证明特性对编译器后端的影响 | 第98页 |
| §4.6 本章小结 | 第98-100页 |
| 第五章 出具证明编译中的证明生成和检查 | 第100-116页 |
| §5.1 携带证明代码的安全性证明原理 | 第100-102页 |
| §5.2 PLCC的目标级验证系统中证明的基本形式 | 第102-105页 |
| §5.2.1 证明的产生过程 | 第102-104页 |
| §5.2.2 证明的形式 | 第104-105页 |
| §5.3 基本块满足规范的证明的产生 | 第105-111页 |
| §5.3.1 证明项的产生过程 | 第105-107页 |
| §5.3.2 指令间断言生成算法 | 第107-108页 |
| §5.3.3 验证条件和证明的生成 | 第108-109页 |
| §5.3.4 证明的内部表示 | 第109-111页 |
| §5.4 全程序证明的生成 | 第111-112页 |
| §5.5 证明检验 | 第112-113页 |
| §5.6 本章小节 | 第113-116页 |
| 第六章 结束语 | 第116-120页 |
| §6.1 论文工作总结 | 第116-118页 |
| §6.2 进一步的工作 | 第118-120页 |
| 参考文献 | 第120-128页 |
| 致谢 | 第128-130页 |
| 攻读学位期间的主要研究工作和论文发表情况 | 第130页 |
