近些年，由于物理瓶颈问题，譬如高温、功耗、漏电等，制造商将关注点从提高单核速度转向多核化等硬件技术。　为了充分释放多核处理器的计算潜力，并行编程技术应运而生。然而，并行执行的不确定性，使得并行软件的测试、调试与分析极为困难。实际上，解决此问题面临着很多巨大的挑战，首先，线程调度难以控制，往往是由操作系统与运行环境所决定；其次，错误难以复现，并行错误在一次执行中被触发，未必会在下次也被触发；最后，交织空间巨大，交织数量与分支及指令数量成双指数关系，遍历所有交织基本是一件不可能的任务
。针对这些挑战，亟需提出行之有效的分析方案，以保证并行软件的可靠性。

本文研究以多线程程序为分析对象，提出了基于SMT（Satisfiability　Modulo　Theories）约束求解的多线程程序自动测试方法，开展了以下研究工作：首先，构建了多线程程序语义-时序约束模型（Semantics-Order　Constraint　Model　for　Multithreaded　Programs），描述了多线程程序执行时所满足程序语义与时序关系。该模型将多线程程序路径与交织的遍历问题转化为约束构建与求解问题，为后续三项案例研究提供了基础。第二，基于语义-时序约束模型，提出了多线程程序前瞻性测试方法Proactive-Testing，使得串行程序测试模式能够在多线程程序上有效。给定输入下执行多线程程序，如果发现错误，则返回错误交织序列以辅助定位错误；否则，可认定该程序在此输入下是正确的，从而可以选择新的输入以继续测试。第三，基于语义-时序约束模型，提出了多线程程序定义-使用关系链测试用例生成方法STEM。STEM以定义-使用关系链为覆盖目标，自动地测试多线程程序，并且生成覆盖每个定义-使用关系链的输入与调度序列；STEM不但减轻了显式穷举路径/交织的复杂度，而且能够使得程序员加深对代码的理解。第四，基于语义-时序约束模型，提出了多线程程序混合式污点分析方法DSTAM，测试在数据流传播过程中由调度时序所产生的安全性问题。DSTAM不但能够确定受时序调度影响的污染变量实例，而且可以生成使其污染的证据序列，以辅助用户分析恶意行为。

论文选取了多个相关研究中常用的C语言多线程程序，进行了实证研究，实验结果表明：Proactive-Testing在检测错误与验证正确性方面皆优于现有方法系统化测试工具Maple与模型检验器ESBMC；STEM穷举定义-使用关系链相比穷举路径/交织更加实用；DSTAM在精度上优于现有的动态污点分析工具DTAM，且能够生成污染实例的证据序列。