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