随着计算机技术的不断进步,计算机系统的软硬件设计越来越复杂,过于复杂和庞大的设计必定会带来越来越多的设计缺陷和错误。传统的方法很难检测到系统设计中的所有错误。然而,系统的安全性在航空、航天、国防、医疗等安全攸关的领域却非常重要。因此,用以保证系统正确性的形式化方法亟待出现。模型检验是上世纪80年代提出的一种针对有穷状态系统进行自动化验证的技术。经过30多年的发展,模型检验技术已经是计算机辅助验证领域非常重要的技术之一。然而,状态空间爆炸问题始终是制约模型检验技术发展的最大障碍。为此,研究人员提出了很多技术来对付该问题,比如基于BDD的符号化模型检验技术、偏序归约技术、抽象精化技术等。近年来,随着SAT技术的进展,Biere[1]等人提出了基于SAT的限界模型检验技术。该技术利用SAT求解器的能力进一步提高了模型检验技术处理问题的规模。目前,基于SAT的符号化模型检验技术已经成为计算机辅助验证领域研究的热点问题之一。然而,在实际应用中,基于SAT的符号化验证技术还存在诸多问题,比如验证效率、验证能力、完全性等。本文围绕基于SAT的符号化模型检验技术进行了一系列研究,旨在进一步提高该技术的效率以及扩展该技术处理问题的能力。本文的主要贡献包括:1)优化了LTL的限界模型检验技术针对现有的LTL的限界模型检验技术,本文提出两种优化的方法。第一种优化技术是一种称为反例集合保持的化简技术,该技术的核心思想就是在进行模型检验之前,首先使用一种轻量级的技术对待验证的LTL性质进行化简,使得化简后的性质与原性质关于待验证的模型是等价的。因此,在真正的模型检验中,就可以使用化简后的性质代替原性质进行验证,该技术对于复杂的性质规约具有非常明显的作用。第二种优化技术,是利用SAT求解器的增量式求解能力,优化了基于语义的限界模型检验编码,实验表明,新的编码在验证效率上,相对于其他编码有很大的优势。这两种技术可以很自然地结合起来,从而提高LTL的限界模型检验效率。2)提出ω-正规性质的限界模型检验算法。由于在工业应用中,许多重要的时序性质无法采用LTL表达,因此,针对ω-正规性质的限界模型检验具有十分重要的理论和实际意义。本文针对两种具有ω-正规表达能力的时序逻辑ETLl+f和QTL,分别提出了对应的限界模型检验算法。针对ETLl+f,本文提出了基于语义的限界模型检验算法。该技术的核心是构造ETLl+f的tableau,通过扩展LTL的tableau构造技术,本文提出了ETLl+f的tableau构造算法。针对QTL,本文提出了两种限界模型检验算法,分别为基于语法的限界模型检验和基于语义的限界模型检验。基于语法的限界模型检验的核心思想是将QTL公式的限界语义编码成QBF公式,然后利用QBF求解器来验证该问题。基于语义的限界模型检验同样是通过扩展LTL的tableau构造方法得到QTL的tableau构造方法,然后将限界模型检验问题转化为受限路径上的公平性路径查找问题。然后,将公平性路径查找问题编码成布尔公式,最后利用SAT求解器来验证该问题。3)提出了基于SAT的符号化模型检验的完全性保证的算法。制约限界模型检验技术应用的一个主要瓶颈在于其不是一种完全的技术,即它不能证明给定的模型是否满足给定的性质。然而,线性时序逻辑的模型检验问题最终都可以转化为公平性路径查找问题,而公平性路径查找问题可以转化为若干个可达性问题。因此,开发高效的可达性算法是解决基于SAT符号化模型检验完全性保证技术的核心。本文基于目前最好的可达性算法,即属性指导的可达性分析算法(Property Directed Reachability,简称PDR),提出了两种新的可达性算法。两种算法的核心思想都是试图通过双向逼近可达状态空间,从而加快算法的收敛速度。实验结果表明,本文提出的可达性算法相对于基本的算法有了很大的提高。4)实现了两个实用的工具。模型检验技术的最终目的是应用,将理论上的算法转化为实用的工具是模型检验技术非常重要的一部分。本文实现了两个实用工具,分别支持本文提出的各个算法。工具ENu SMV是基于开源的符号化模型检验工具Nu SMV实现的,它支持本文提出的C?PR?(Counter?xample Preserving R?duction,简称C?PR?)算法、增量式的基于语义的LTL限界模型检验算法、基于语义的ETLl+f的限界模型检验算法。工具Reach是一个全新的基于SAT的符号化模型检验工具,它不仅支持本文提出的交叠的PDR算法以及并行的PDR算法,还支持其他著名的可达性算法,包括限界模型检验算法、k步归纳算法、基于插值的符号化模型检验算法以及基本的PDR算法。