基于类型系统的程序验证方法研究
| 论文创新点 | 第6-7页 |
| 目录 | 第7-10页 |
| 摘要 | 第10-11页 |
| ABSTRACT | 第11-12页 |
| 1 绪论 | 第13-25页 |
| 1.1 研究背景 | 第13-15页 |
| 1.2 研究动机 | 第15-16页 |
| 1.3 相关研究工作 | 第16-23页 |
| 1.4 论文主要创新点 | 第23-24页 |
| 1.5 论文组织结构 | 第24-25页 |
| 2 类型安全内存模型 | 第25-76页 |
| 2.1 引言 | 第25-26页 |
| 2.2 经典内存模型 | 第26-33页 |
| 2.2.1 字节序列模型 | 第26-28页 |
| 2.2.2 分块内存模型 | 第28-30页 |
| 2.2.3 Burstall内存模型 | 第30-33页 |
| 2.3 内存数据类型 | 第33-37页 |
| 2.4 内存数据表示 | 第37-40页 |
| 2.5 抽象内存模型 | 第40-58页 |
| 2.5.1 抽象内存模型定义 | 第40-42页 |
| 2.5.2 内存访问控制 | 第42-45页 |
| 2.5.3 抽象内存操作定义 | 第45-47页 |
| 2.5.4 抽象内存模型基本性质 | 第47-58页 |
| 2.6 具体内存模型 | 第58-64页 |
| 2.7 内存模型评估及应用实例 | 第64-75页 |
| 2.7.1 内存模型在程序验证中的应用 | 第64-67页 |
| 2.7.2 内存模型在语言语义上的应用 | 第67-75页 |
| 2.8 本章小结 | 第75-76页 |
| 3 用于程序验证的类型系统 | 第76-122页 |
| 3.1 引言 | 第76-77页 |
| 3.2 类型理论基础知识 | 第77-85页 |
| 3.2.1 依赖类型 | 第79-81页 |
| 3.2.2 精化类型 | 第81-82页 |
| 3.2.3 子类型 | 第82-84页 |
| 3.2.4 动态类型 | 第84-85页 |
| 3.3 语法 | 第85-89页 |
| 3.3.1 表达式 | 第86-87页 |
| 3.3.2 语句 | 第87-88页 |
| 3.3.3 声明语句和整个程序 | 第88-89页 |
| 3.4 类型系统 | 第89-99页 |
| 3.4.1 类型抽象语法 | 第90-91页 |
| 3.4.2 类型环境及类型相关辅助函数 | 第91-92页 |
| 3.4.3 类型合法性规则及子类型规则 | 第92-93页 |
| 3.4.4 常量类型规则 | 第93-94页 |
| 3.4.5 表达式类型规则 | 第94-96页 |
| 3.4.6 语句类型规则 | 第96-98页 |
| 3.4.7 整个程序的类型规则 | 第98-99页 |
| 3.5 动态语义 | 第99-109页 |
| 3.5.1 语义定义基本要素 | 第100-101页 |
| 3.5.2 表达式左值求值规则 | 第101-102页 |
| 3.5.3 表达式右值求值规则 | 第102-104页 |
| 3.5.4 语句语义规则 | 第104-109页 |
| 3.6 类型系统可靠性证明 | 第109-119页 |
| 3.7 应用实例 | 第119-121页 |
| 3.8 本章小结 | 第121-122页 |
| 4 基于类型的程序验证 | 第122-176页 |
| 4.1 引言 | 第122-123页 |
| 4.2 程序验证基础知识 | 第123-133页 |
| 4.2.1 模型检验 | 第123-126页 |
| 4.2.2 定理证明 | 第126-130页 |
| 4.2.3 程序分析 | 第130-133页 |
| 4.3 BOOGIE介绍 | 第133-136页 |
| 4.4 基于类型的程序验证 | 第136-141页 |
| 4.5 标准C语言类型检测过程 | 第141-147页 |
| 4.5.1 类型的转换 | 第142-143页 |
| 4.5.2 表达式的转换 | 第143页 |
| 4.5.3 语句的转换 | 第143-144页 |
| 4.5.4 声明语句及整个程序的转换 | 第144-146页 |
| 4.5.5 转换示例 | 第146-147页 |
| 4.6 基于BOOGIE的类型检测 | 第147-171页 |
| 4.6.1 内存模型建模 | 第148-151页 |
| 4.6.2 表达式语义转换 | 第151-155页 |
| 4.6.3 表达式类型检测转换 | 第155-157页 |
| 4.6.4 语句的转换 | 第157-160页 |
| 4.6.5 函数调用语句转换 | 第160-161页 |
| 4.6.6 变量声明语句转换 | 第161-166页 |
| 4.6.7 函数声明语句转换 | 第166-169页 |
| 4.6.8 整个程序的转换 | 第169-171页 |
| 4.7 应用实例 | 第171-173页 |
| 4.8 实验结果与分析 | 第173-175页 |
| 4.8.1 实验基准数据集 | 第173-174页 |
| 4.8.2 实验环境与方案 | 第174页 |
| 4.8.3 实验结果 | 第174-175页 |
| 4.9 本章小结 | 第175-176页 |
| 5 总结与展望 | 第176-179页 |
| 6 参考文献 | 第179-189页 |
| 7 攻博期间发表的科研成果及参与的项目 | 第189-191页 |
| 7.1 科研成果(论文、专著) | 第189-190页 |
| 7.2 项目 | 第190-191页 |
| 致谢 | 第191-192页 |
