软件已经成为国防建设和国计民生的重要组成部分。然而,随着软件技术的快速发展,软件的规模越来越大,复杂度越来越高,软件安全问题日益凸显。如何保障软件的安全性,稳定性和可靠性已经成为亟待解决的问题。模型检测是一种重要的形式化验证技术,该技术已经成功应用于软硬件的验证。模型检测的思想是基于对状态空间的穷举搜索,其面临的主要挑战是状态空间爆炸问题。基于反例引导的抽象细化框架CEGAR是应对这一挑战的重要方法,而Craig插值被应用于抽象模型的细化过程。为了进一步提高模型检测的验证效率,本文基于Craig插值和CEGAR框架提出一种新的验证算法。本文的主要工作内容和创新点如下:1.提出两种新的插值用于标记程序路径是否安全:True插值和Error插值。其中,True插值用于判断从一个程序位置出发的所有路径是否安全,Error插值用于判断从一个程序位置出发是否存在一条错误路径。2.利用新定义的两种插值提出一种路径剪枝算法,用于减少搜索路径的规模以提高检测效率。对于True插值,如果是全插值且被当前节点的路径前缀蕴含,则该节点下的执行子树都可以被归并。对于Error插值,如果当前节点的路径前缀蕴含Error插值,则路径不安全。3.为了加快算法中全插值节点的形成,本文提出一种基于权值的优化算法。主要思想是:为程序控制流图的每一条边添加权值属性,表示当前边的后续控制流图中未被遍历的分支个数。在遍历控制流图的过程中,根据权重的大小来决定分支的遍历顺序。本文通过验证时间和成功验证率两个指标来分析算法效果,实验结果表明本文算法相比原算法,在验证时间上缩短12%,在成功验证率上提高4%,本文算法卓有成效。