形式化验证方法主要包括定理证明和模型检验,其中模型检验因其自动化高得到重视,并已经在硬件领域和通讯协议的分析与验证中取得了巨大成功。近几年来,软件模型检验成为研究的热点,并取得一定的成功。软件系统通常涉及无穷数据域上的运算而呈现出无限状态,而模型检验方法只能对有限状态模型进行验证,因此软件模型检验面临的最大问题是状态空间爆炸。抽象是最有潜力的解决状态爆炸问题的方法。谓词抽象的提出实现了抽象的自动化。当前基于谓词抽象的反例导向抽象精化方法是软件模型检验的主要方法。本文主要研究内容如下。　　(1)基于抽象解释和谓词抽象理论,对谓词抽象算法和反例导向抽象精化算法进行了研究。　　(2)对软件模型检验工具BLAST做了研究,该工具使用惰性抽象技术将反例导向抽象精化方法中的抽象模型构造,模型检验,抽象精化三个过程整合成为一体,on-the-fly构造抽象模型,按需求精化。如果模型检验输出虚假反例,则进行谓词精化实现抽象模型的精化。BLAST的抽象系统构造使用传统的定理证明器作为求解器,本文研究了将SAT求解器应用于BLAST的抽象模型构造,这种方法可以克服定理证明器的局限性,并且可以构造一个更精确的抽象模型,提高计算效率。　　(3)在抽象模型构造-模型检验-谓词精化的迭代过程中,如果抽象模型不够精确,模型检验将产生抽象虚假反例,其在原始系统中没有对应的具体反例,这时需要进行谓词精化,增加谓词用于去除虚假反例。用更新后的谓词集合重新构造一个没有虚假反例的抽象模型,重新进行模型检验。相对其他谓词精化方法而言,BLAST的谓词精化算法基于克雷格插值,效率较高。但是现有的谓词精化方法都是发散的。本文对基于插值的谓词抽象精化完备性进行了研究,使用拆分证明,将插值约束于有限的语言,避免了新生成的谓词发散,保证了完备性。