多线程程序是计算机软件设计的核心,如何高效验证多线程程序的安全性问题已成为国内外研究人员的主要研究内容。现有研究表明:多线程程序的安全性问题可简化为良拟序迁移系统(Well-Quasi-Ordered Transition System,WQOTS)的可覆盖性问题。针对良拟序迁移系统的可覆盖性问题,已存在大量的解决方案,它们主要是以显示状态搜索思想设计的。多线程程序的状态空间随程序的规模和线程数目的增加呈指数级增长,导致这些算法都存在低效性或不完备性的问题。如何在验证过程中尽量避免状态空间搜索或降低状态空间的规模是提高多线程程序安全性验证效率的关键。本文主要的研究对象是被无穷个线程并发执行的有限状态布尔程序(Boolean Program,BP),可以通过对多线程程序进行谓词抽象得到。本文根据目前多线程程序验证方法的优势和不足,考虑到基于SMT求解器的符号分析方法能避免对状态空间搜索从而加快验证,以及直接使用布尔程序作为抽象模型能降低状态空间的规模,提出了一种新的多线程程序安全性验证方法。首先研究了基于SMT求解器的符号分析模块,详细分析了如何利用计数抽象从线程迁移系统中构造可覆盖性问题的线程状态等式,该线程状态等式使用SMT求解器处理后,可根据求解器的输出结果判断多线程程序的安全性;由于线程状态等式是对可覆盖性问题的过近似(over-approximate),无法验证不安全程序,因此提出了一种基于BP的高效且完备的KM算法。其次进一步研究了BP与线程迁移系统之间的关联,通过分析线程迁移系统中的全局状态和BP中的程序状态之间的转换规则,研究了如何将作用在线程迁移系统上的KM算法直接作用在BP上,并分析了KM算法中最大覆盖后继的计算方法。由于正向搜索中,可覆盖性问题与初始线程数目有关,为了降低搜索过程中内存使用,借助SMT求解器处理线程状态等式能输出一个可覆盖性的解模型,对KM算法进行了改进;使用SMT求解器输出的初始线程数目作为KM算法的初始线程数目,在搜索过程中,如果不满足则再进行一次完整的KM算法,从而得到一个高效的不安全程序验证模块。最后对本文提出的结合基于SMT的符号分析模块和基于BP的显示状态搜索模块工具进行设计和实现。实验结果显示:本文提出的方法不仅能减少多线程程序验证的时间,还能降低验证过程中内存的使用。