随着社会信息化程度的不断提高,计算机在各行各业扮演的角色越来越重要,软件系统的安全问题也因此愈发受到重视。而C语言在航空航天、地铁运输、国防安全等关键领域使用广泛,因此保障C代码的正确性非常重要,研究人员基于传统模型检验技术研发了多款面向C代码的模型检验工具如CBMC、CPAChecker等等。但以上方法和工具都是针对代码转化得到的整体问题进行验证,随着代码规模的不断扩大会导致状态空间爆炸的问题,使得问题规模超出底层求解器支持,验证效率低下。为此,在之前的工作中,我们已经提出了一种面向路径的有界模型检验算法SAT-LP-IIS,该算法将单次验证对象限制为一条程序执行路径,能够一定程度上控制验证复杂度,并以此为基础实现了一个简单工具原型。然而在我们将该方法实际应用于C代码的模型检验时,仍有很多挑战需要面对,首先是该方法在处理规模较大的代码时,需要遍历验证的路径数量很大,可能存在路径爆炸的问题,因此需要更加高效的路径遍历方法;同时,当输入的代码中包含迭代次数较大的循环结构时,路径的长度可能很大,导致单次验证的难度提升,因此需要有效处理循环的方法和框架。为解决上述问题,同时将方法实际应用于C代码上的有界模型检验,本文主要做了如下工作:针对目前存在的路径爆炸的问题,本文提出了一种新型的路径遍历方法。该方法基于并行计算技术,通过并行验证多条路径加快验证,同时使用共享不可行路径池,同步反馈各路径验证结果以避免不必要的计算,从而提高整体的验证效率。针对目前无法有效处理迭代次数较大的循环结构的问题,本文提出了一种针对循环结构的集成处理框架。该框架利用循环总结技术和循环抽象技术,在验证之前对循环进行预处理,从而提高系统对循环结构的处理能力。为了将上述方法落实到实际C代码的有界模型检验上,同时为了评估本文工作的效果,我们按照优化后的算法和框架实现了一个面向C代码的有界模型验证工具BRICK,并添加了多种通用技术进行整体支持。我们为优化前后的BRICK与一些具有代表性的同类工具设计了实验并将结果进行对比,结果显示基于本文方案的BRICK有着良好的性能优势。