| 摘要 | 第1-11页 |
| ABSTRACT | 第11-14页 |
| 第一章 绪论 | 第14-34页 |
| ·课题研究背景 | 第14-16页 |
| ·软件的可信性质 | 第14-15页 |
| ·基于软件源代码的可靠安全性质保证 | 第15-16页 |
| ·相关研究工作 | 第16-25页 |
| ·静态分析方法 | 第17-18页 |
| ·定理证明方法 | 第18-19页 |
| ·抽象解释方法 | 第19-20页 |
| ·模型检验方法 | 第20-24页 |
| ·谓词抽象方法 | 第24-25页 |
| ·课题研究思路 | 第25-30页 |
| ·相关工作的小结与比较 | 第25-27页 |
| ·课题研究目标 | 第27-28页 |
| ·课题研究内容 | 第28-29页 |
| ·课题技术特色 | 第29-30页 |
| ·课题创新点 | 第30-32页 |
| ·论文结构 | 第32-34页 |
| 第二章 切片执行的基本概念和方法 | 第34-57页 |
| ·基本模型和概念 | 第35-37页 |
| ·C 程序模型和时序安全性质 | 第35-36页 |
| ·最强后置条件 | 第36-37页 |
| ·基于变量抽象的程序保守近似语义 | 第37-41页 |
| ·变量抽象 | 第37-38页 |
| ·部分最强后置条件 | 第38-41页 |
| ·切片执行 | 第41-46页 |
| ·切片执行上下文 | 第41-42页 |
| ·切片执行图 | 第42-44页 |
| ·讨论 | 第44-46页 |
| ·时序安全性质的验证 | 第46-51页 |
| ·对切片执行图的模型检验 | 第46页 |
| ·切片执行与模型检验的集成 | 第46-48页 |
| ·抽象准则的精化 | 第48-51页 |
| ·验证工具与实验结果 | 第51-54页 |
| ·验证工具 | 第51-52页 |
| ·实验结果与分析 | 第52-54页 |
| ·相关工作 | 第54-56页 |
| ·小结 | 第56-57页 |
| 第三章 搜索复用框架及其在切片执行中的应用 | 第57-70页 |
| ·面向切片执行的搜索复用框架 | 第57-59页 |
| ·基于搜索复用框架的切片执行 | 第59-63页 |
| ·可靠状态的确定 | 第63-66页 |
| ·实验结果 | 第66-68页 |
| ·相关工作 | 第68-69页 |
| ·小结 | 第69-70页 |
| 第四章 部分最弱前置条件及其在切片执行中的应用 | 第70-89页 |
| ·部分最弱前置条件 | 第71-73页 |
| ·部分最弱前置条件在切片执行中的应用 | 第73-78页 |
| ·避免部分最弱前置条件公式规模的指数增长 | 第78-82页 |
| ·最弱前置条件公式规模的指数增长问题与解决方法 | 第78-79页 |
| ·紧凑的部分最弱前置条件表示和计算方法 | 第79-82页 |
| ·处理指针与变量别名 | 第82-84页 |
| ·实验结果与分析 | 第84-87页 |
| ·相关工作 | 第87页 |
| ·小结 | 第87-89页 |
| 第五章 有状态动态偏序缩减方法 | 第89-112页 |
| ·并发C 程序模型和无状态动态偏序缩减方法 | 第91-94页 |
| ·并发C 程序模型 | 第91-92页 |
| ·无状态动态偏序缩减方法 | 第92-94页 |
| ·有状态动态偏序缩减方法 | 第94-100页 |
| ·交迭信息总结 | 第94-98页 |
| ·有状态动态偏序缩减方法 | 第98-100页 |
| ·有状态动态偏序缩减的实现 | 第100-107页 |
| ·交迭信息总结的实现 | 第100-102页 |
| ·基于有状态动态偏序缩减的含圈状态空间遍历过程的实现 | 第102-107页 |
| ·实验结果 | 第107-110页 |
| ·相关研究工作 | 第110页 |
| ·小结 | 第110-112页 |
| 第六章 并发C 程序的切片执行 | 第112-130页 |
| ·并发C 程序模型及其保守近似语义 | 第113-116页 |
| ·并发C 程序模型 | 第113-114页 |
| ·变量抽象下的保守近似语义 | 第114-116页 |
| ·并发C 程序的基本切片执行 | 第116-117页 |
| ·集成无状态动态偏序缩减的切片执行 | 第117-121页 |
| ·时钟向量 | 第117-118页 |
| ·集成无状态动态偏序缩减的切片执行 | 第118-121页 |
| ·集成有状态动态偏序缩减的切片执行 | 第121-125页 |
| ·基于时钟向量的有状态动态偏序缩减方法的实现 | 第121-122页 |
| ·集成有状态动态偏序缩减方法的切片执行过程 | 第122-125页 |
| ·建模环境与实验结果 | 第125-128页 |
| ·并发C 程序建模环境 | 第125-126页 |
| ·实验结果 | 第126-128页 |
| ·相关研究工作 | 第128-129页 |
| ·小结 | 第129-130页 |
| 第七章 面向切片执行的轻量级判定过程 | 第130-143页 |
| ·完备的整数线性公式判定方法 | 第131-134页 |
| ·面向C 源代码验证的扩充判定方法 | 第134-136页 |
| ·对切片执行产生的一阶逻辑验证公式的判定 | 第136-139页 |
| ·验证工具和实验结果 | 第139-141页 |
| ·相关工作 | 第141-142页 |
| ·小结 | 第142-143页 |
| 第八章 结束语 | 第143-145页 |
| ·工作总结 | 第143-144页 |
| ·研究展望 | 第144-145页 |
| 致谢 | 第145-147页 |
| 参考文献 | 第147-156页 |
| 作者在学期间取得的学术成果 | 第156-157页 |