符号执行技术是一种被应用在串行和并发程序上的系统测试技术。但是在并发环境下传统符号执行会产生状态空间爆炸问题,测试效率会受到很大影响。引发这种状态空间爆炸问题的主要原因是传统符号执行尝试搜索所有可能的线程交织路径,而路径数量会随着并发程序中线程数量的增长呈指数性增长。因此如何改进传统符号执行算法又不影响测试的准确性是很具有意义的研究点。在本文的研究中,我们提出了一个名为SYMAC的并发程序测试框架,框架的核心思想是将传统的符号执行算法进行改进,结合我们定义的分层并发覆盖准则,来改善传统符号执行算法会出现的状态空间爆炸的问题,并且我们还以最弱前置条件为基础,提出了基于预测摘要的剪枝框架,通过这个框架来在搜索路径的过程中提前终止不必要的搜索过程,来达到进一步提升测试效率的目的。在我们的工作中,首先定义了一个访存冲突前驱集合的概念,然后以访存冲突前驱集合为基础,类比串行覆盖准则思想去构建了一套分层并发覆盖准则。通过分层覆盖准则,我们对原始并行符号执行算法进行改进,达到有选择性地搜索线程交织路径的目的。为了进一步的缩减状态空间大小,我们提出一个基于预测摘要的剪枝框架。该剪枝技术在已执行过但未违反断言条件的路径上,总结并存储某些特定全局控制状态点的预测摘要,然后预测摘要可以为搜索后续线程交织路径提供一个是否能够提前终止的判定条件。根据前面理论框架的研究,我们将该并发程序测试框架实现,并且通过对benchmark中一定数量的多线程C/C++程序进行了实验性的评估。实验的结果表明,我们的并发测试框架既能有效的减少系统的开销,也能得到很好的并发错误检测性能。