基于模型检测的C程序循环检测方法的研究与实现

摘要

计算机技术的快速进步，使人离不开计算机，各式各样的软件层出不穷，软件规模也与日俱增，仅以测试的方法排查漏洞已经不能满足需要。为了减少软件中的漏洞，保证软件程序的正确性和可靠性，很多研究人员对基于源代码的软件模型检测方法进行了深入的研究并取得了很好的成绩。
　　基于反例驱动的抽象细化算法，是近年来被广泛使用的检测算法。它通过 Craig插值来计算谓词,并用谓词对程序进行抽象。该算法不但缓解了状态空间爆炸问题，还能保持检测结果的精确性。但是，对于程序中的循环结构的检测，还是会由于状态数太多，而导致检测效率低。为了缓解此问题，本文提出一个新的算法，该算法在基于反例驱动的抽象细化算法的基础上，采用静态分析与动态执行相互结合的方法对C语言程序验证，并改善了对程序中循环的检测，提高检测效率。
　　本算法将循环分成两个类别，一类为简单循环，对于这部分的处理使用静态分析，在建立模型的过程中，对简单循环部分的模型进行改良，替换原来的模型，减少在对循环检测时的展开，从而节约大量空间以及展开过程中耗费的时间。另一部分为复杂循环，对于这部分的处理使用动态执行的方法，在进入复杂循环的临界点上提取程序信息，将循环体代码与其上下文两部分结合形成完整的执行代码，并将其编译执行，执行之后输出的有效信息抽象成模型的状态，继续参与后续的验证。本文将提出的算法编码实现，并做了大量实验，得到了不错的结果。

目录

声明

插图索引

表格索引

缩略语对照表

第一章 绪论

1.1课题研究的意义和背景

1.2国内外研究与发展现状

1.3研究内容和目标

1.4论文结构

第二章 相关技术与工具

2.1 CPAChecker简介

2.2 CIL工具简介

2.3求解器介绍

2.4本章小结

第三章 基于模型检测的C程序循环检测方法

3.1抽象模型检测方法

3.2以CPAChecker为例的CEGAR算法

3.3改进的算法框架

3.4简单循环的检测流程

3.5本章小结

第四章 简单循环的检测和实现

4.1简单循环处理的总体算法

4.2模拟执行次数的计算方法

4.3简单循环的处理

4.4本章小结

第五章 实验结果与分析

第六章 总结与展望

6.1总结

6.2展望

参考文献

致谢

作者简介