随着多核计算的兴起，并发软件成为计算机辅助验证的重要目标。并发软件系统在社会生活、国民经济等诸多关键领域的应用愈加普遍，软件系统存在的微小错误或漏洞可能会引起重大的经济损失甚至难以预计的后果，检测软件缺陷的形式化验证技术成为学术界和工业界备受关注的热点。　　近年来，大型并发软件系统普遍采用任务驱动或者事件驱动的编程方法，本文的研究重点是针对并发程序的形式化验证技术，通过对其抽象模型进行高效的可达性分析，确定抽象模型是否满足预期的性质或者规格。可达性分析是一种常见的程序验证技术，通过搜索程序执行产生的状态空间，确定程序是否会到达某些错误的状态，从而查找程序中的错误或漏洞。论文针对并发程序的可达性分析进行研究，取得如下创新成果：　　1.针对Fork/Join并行模式的并发程序的可达性问题进行分析，将可以模拟Fork/Join并行线程创建的并发程序执行的抽象模型（动态并发下推系统）化简为对应的并发下推系统，化简后的系统可以使用现有的k-定界可达算法进行求解。　　2.采用上下文定界方法抑制状态空间爆炸问题，通过约束系统进程的消息队列是良序的，证明其上下文切换定界可达性问题是可判定的。提出一种构造模拟递归队列并发程序执行的多栈下推系统的转换方法，将其上下文切换定界可达性问题转换为多栈下推系统的阶定界可达性问题。　　3.基于上下文定界思想和良序排队约束，提出一种针对多栈下推系统的上下文切换定界可达算法，对下推系统迭代地应用标准Post*算法，穷尽地计算k次上下文切换内正向可达的格局，通过对目标状态集合与可达格局集合的交集进行判空，最终解决递归队列并发程序的可达性问题。