软件已经成为当今社会发展中不可或缺的元素,在航空航天、医疗、交通等关键领域已经得到成功的运用。随着软件的重要性日益凸显,软件的可靠性和安全性自然而然地受到重视。长期以来,研究人员一直着眼于如何发现软件中隐藏的错误,保障软件的可靠性和安全性。模型检测是应用广泛且十分有效的方法之一。它通过对程序建模,形式化地描述性质,然后自动化地验证程序是否满足期望的性质。但是,状态空间爆炸问题是模型检测面临的一个关键问题,严重影响了模型检测方法的验证能力,降低了其对大规模程序的验证效果。因此,如何提高模型检测方法的验证效率和验证规模,使得其能更好地应用于大规模的程序验证,已经成为程序验证领域的研究热点。反例制导的抽象细化(Counterexample-guided Abstraction Refinement,CEGAR)技术能有效地缩减模型检测的状态空间,提高模型检测的效率,对大规模程序也有很好的应用性。本文重点围绕基于CEGAR的抽象模型检测方法,研究和讨论如何缓解状态空间爆炸问题,以及如何自动化地对程序的性质进行验证。本文的主要贡献和研究内容如下:第一,基于CEGAR的模型检测方法已经成功地应用于大规模的程序验证,借助于Craig插值能有效地构造抽象谓词。为了进一步系统地缩减在安全性验证过程中产生的状态空间,本文提出了两种新的Craig插值应用:安全插值和错误插值。当某一个位置的安全插值被当前路径蕴含时,说明所有从当前位置出发的路径都是安全的。同样地,当某一个位置的错误插值被当前路径蕴含时,说明从当前位置出发的路径中存在一条不安全的路径,即可以到达目标状态。同时,本文提出了两种优化策略,保障新的插值能得到更好的应用。本文主要讨论了如何计算和应用这两种插值对程序的安全性进行验证,实现了新的算法,并开发了模型检测工具INTERPCHECKER。最后,通过大量的实验表明,新的插值和优化策略能有效地提高软件模型检测的验证规模。第二,为了对C程序中的安全性质和时序性质都能进行自动化地验证,本文研究了针对安全性质的分析方法,将其扩展到对时序性质的验证。首先,针对C程序空指针解引用问题,采用线性时序逻辑(Linear Temporal Logic,LTL)对其进行描述,然后将控制流图(Control Flow Graph,CFG)和LTL公式相结合,验证程序是否存在空指针解应用问题。紧接着,扩展该方法,将LTL扩展到有穷模型,给出了一种能有效地将LTL转化为确定化有穷自动机(Deterministic Finite Automata,DFA)的算法;并将该算法和基于CEGAR的模型检测方法相结合,对一般的C程序时序性质进行验证。最终,本文实现了新的算法,并开发了支持C程序时序性质验证的模型检测器TPCHECKER。通过实验,说明了新方法在非安全性质的验证方面具有很好的优势,且对于安全性质的验证,比传统插桩的方法更有效。第三,模型检测方法主要是用于发现程序的错误。一个所期望的性质,可以被形式化地表示为时序逻辑公式,也可以通过插桩的形式来检测。当一条路径违背被定义的性质时,它被称为反例路径。如何在模型检测中快速地发现一条反例路径是一个非常有意义的研究课题。反例路径检测的主要挑战是程序中的循环。与循环相关的计算和数据可能会造成状态空间急剧增长。这意味着当遇到深度循环时,大多数的工具将耗尽内存或返回不精确的结果。为了进一步地提高模型检测的效率,缩减状态空间,本文提出了一种既能快速生成反例又能保持较高精度的动静结合方法。首先将循环根据规则分为简单循环和复杂循环。对于简单循环,生成其循环摘要,避免展开循环。对于复杂循环,采用动态执行的方法,加快寻找反例路径的速度。为了在实践中评估其性能,本文实现了所提出的方法并开发了工具HYVER。通过在大量基准测试程序上的实验表明,新的方法在加速反例检测方面是非常有用的。