随着多处理器和多核计算的兴起,并发程序的验证逐渐成为学术界广泛关注的热点问题之一。然而,由于并发程序本身存在的线程交互性,使得程序的执行不具备确定性,即在相同的输入下,程序多次执行后的结果可能不同,或者执行结果相同但内部执行路径不同,上述两种情况都直接导致了传统的测试技术无法精确地发现并发程序中隐藏的错误和漏洞。因此,尽可能采用一种实用的形式化验证方法和理论技术来解决并发程序研发过程中潜在的问题,显得尤为重要与迫切。　　在并发程序的验证技术中,可满足性分析是一项重要的核心技术,其基本思想主要是通过分析某一个给定的性质是否满足该并发程序模型,从而判定该程序是否存在错误或漏洞。本文分别针对基于共享变量和消息队列通信方式的并发程序进行可满足性分析,旨在通过可满足性分析保证此类程序的正确性和可靠性。基于上述思想,本文的研究工作主要包括:　　(1)针对基于消息队列进行线程间交互的并发程序,本文采用了基于SMT(Satisfiability Modulo Theories)的有界模型队列对其进行可满足性公式编码。由于当前的SMT求解器所采用的SMT-LIB格式的输入语言并不直接支持队列理论,因此,为了能够准确地编码消息队列的行为,本文结合SMT求解器中的相关理论域,如未解释函数(uninterpreted function)和数组(array),分别提出两种不同的编码方法:shifting编码和cyclic编码。对于前一种编码方式,主要是采用不依赖于任何理论的布尔和位向量显式地表示队列中的内容,该技术可以直接应用于基于 BDD(Bounded Model Checking)或SAT/SMT的验证过程中;而对于后一种编码方式,本文重点采用基于未解释函数和数组的内容表示方法。最后对这两种编码方式进行了复杂度的比较。　　(2)针对基于共享变量进行线程间交互的并发程序,本文采用了基于SMT的并发程序可满足性验证。由于SMT在表达能力上使用了含有量词和变量的一阶逻辑,能处理更加复杂的性质验证,并且提高程序验证的准确度,因此本文主要采用基于SMT的验证技术,同时为了能有效地限定允许交互的上下文切换数目、进一步约简验证并发程序的复杂度,本文还结合上下文限界(context-bounded)的思想,以及极小不可满足核(minimal unsatisfiable clauses)的查找技术,提出了一种针对并发路径程序模型(CTP)的可满足性判定算法。并且通过复杂度分析理论上证明该算法在一定程度上能够缓解对并发程序可满足性验证的复杂性。最后通过一个实例阐述了该方法的有效性。