随着计算机系统的广泛应用,计算机软件的高可信性质受到了越来越多的关注。面向软件源程序的形式验证是保障软件高可信性质的一种有效方法,受到了大量的关注和广泛的研究。但是,由于软件程序逻辑复杂、规模庞大,如何提高软件源程序验证的精度特别是可扩展性仍是当前研究所面临的主要问题。本文提出了一种面向C程序的时序安全性质验证方法,即切片执行方法。它本质上是一种轻量级的符号执行,能够自动抽象出顺序和并发C程序的有限状态模型,并基于模型检验方法进行验证。切片执行融合了程序切片、程序语义抽象、符号化状态表示、反例制导的抽象精化、偏序缩减等多种有效的状态空间缩减技术,大大缩减了抽象模型的状态空间,从而提高了软件源程序形式验证的可扩展性。切片执行的主要特点是面向时序安全性质的验证,能够以接近标准流敏感数据流分析的代价,达到路径敏感程序模拟的验证精度;同时切片执行支持包括循环在内的程序结构,支持全自动的模型抽象和性质验证。切片执行构建在基于变量抽象的程序保守近似语义的基础上,它符号化地执行变量抽象下的相关语句,计算用于描述程序保守近似语义的部分最强后置条件和部分最弱前置条件,抽象出C程序的有限状态模型,并基于模型检验方法验证抽象模型是否满足给定的时序安全性质。基于本文提出的搜索复用框架,切片执行不断根据产生的伪反例路径精化变量抽象的抽象准则,直到性质被验证或找到真实反例路径。面向并发C程序验证,切片执行集成了本文提出的有状态动态偏序缩减方法,大大缩减搜索的状态空间。切片执行还集成了一种轻量级判定过程,用于对C程序验证过程中的验证公式进行高效判定。具体地,本文的创新点包括如下五个方面:1、提出了切片执行的基本概念和方法。基于对程序验证基本规律的分析,我们提出了变量抽象方法,只考虑程序中与待验证性质相关的变量和语句。基于变量抽象,我们定义了部分最强后置条件,进而定义了程序的保守近似语义。基于这两个概念,我们提出了切片执行的概念,它是一种轻量级的符号执行过程。2、提出了面向时序安全性质验证的搜索复用框架并将其应用于切片执行。搜索复用框架也是一种反例路径制导的抽象精化(CEGAR)框架,基于伪反例路径进行模型精化。相比传统的CEGAR框架,搜索复用框架的最大特点是能够在不同精度的抽象模型之间进行充分的信息复用,从而避免了大量不必要的重复搜索,有效降低了验证开销。3、提出了部分最弱前置条件的概念并将其应用于切片执行。部分最弱前置条件是程序保守近似语义的另一种表示方法,同样基于变量抽象定义。在切片执行过程中,可以用部分最弱前置条件部分地取代部分最强后置条件,以生成更弱的一阶逻辑公式来描述抽象模型的同一个状态,从而在不影响模型精度的前提下有效缩减生成模型的状态空间。4、提出了面向有状态模型检验的有状态动态偏序缩减方法,并将其集成到切片执行过程中。我们将切片执行方法扩展到了对并发C程序的验证。为了进一步进行状态空间缩减,我们提出了有状态动态偏序缩减方法,并将其自然地集成到切片执行框架中,用于指导切片执行,使其避免搜索多条具有相同偏序关系的并发进/线程交迭执行路径。我们进行了多个实验,包括两个实用并发程序片段和一个并发SSL程序。实验结果表明,切片执行和有状态动态偏序缩减这两种正交的状态空间缩减方法的集成,大大缩减了并发程序抽象模型的状态空间,特别是降低了验证的空间开销。5、提出了面向切片执行验证公式的轻量级判定过程。我们定义了一类整数线性一阶逻辑判定公式,此类判定公式支持C程序中常用的整数线性运算。我们优化了判定过程,并扩充了对整数除法、取余和位运算的支持。实验表明,扩充后的判定过程能够对面向C程序的切片执行所产生的绝大多数验证公式进行高效判定。在基于SSL程序的切片执行实验中我们发现,采用该判定方法后,验证效率比使用定理证明工具Simplify提高了10.5倍。我们还基于开放源代码的MAGIC项目,实现了基于切片执行的C程序验证工具原型,并基于openssl-0.9.6c等实用程序针对上述每个创新点都进行了实验。我们在实验时采用了与BLAST和MAGIC相同的硬件平台,并针对相同的验证用例,验证了相同的性质集合。经过充分的实验数据对比,我们发现切片执行在验证效率上具有一定的优势。