软件复杂度的增加及多核体系结构的广泛应用，使得通过传统模式检查软件正确与否变得愈加困难。本论文研究了并发程序自动分析与验证的相关理论、技术及工具。本文的工作主要关注在两个方面:如何自动验证并发递归程序的安全性性质，以及如何自动分析并发数据结构的可线性化性质。　　 并发递归程序安全性性质的自动验证是难问题，因为其可以等价到上下文无关语言交集判空问题上，而后者是不可判定问题。我们基于语言理论，利用反例制导的抽象精化框架，给出了验证并发递归程序安全性性质的半判定算法。首先，将潜在的错误区域抽象为上下文无关语言，如果抽象为空，则说明原系统安全。否则需要对反例进行判断，我们利用限界语言表示潜在的反例集合，并检查限界语言与多个上下文无关语言之间的交集是否为空。如果非空，则说明原系统不安全，否则说明通过限界语言描述的反例是假反例，需要将其从抽象中剔除并继续寻找新的限界语言。在抽象精化过程中，不同的上近似及限界近似会对结果产生不同的影响，例如，影响检测过程是否终止。我们研究了已有的算法，并提出了两种上近似算法及一种限界近似算法。最后，我们实现了模型检测工具LCegar，并对实际的并发递归程序进行了验证。　　 可线性化是刻画并发数据结构正确性的一种标准，本文从自动分析及测试的角度考虑如何检查并发数据结构的可线性化性质。在“并发数据结构的顺序行为是相对容易验证”的前提假设下，我们将关注点集中在寻找并发历史的顺序化执行上。对数据结构的一条并发执行历史，如果存在合法的顺序化执行与其对应，则说明这条历史是可线性化的，如果不存在，则说明并发数据结构是不可线性化的。在对常见的并发算法进行分析后，本文提出了两种加速策略:猜测线性化点及读写分离，然后提出了一种自动分析的算法，将对并发历史的检查工作划分为两个阶段，利用第一阶段提高检查的效率，利用第二阶段保证检查的可靠性。最后，我们实现了相应的测试工具VeriTrace，并对实际的Java程序进行了测试，实验结果显示我们的算法在高并发环境下具有很高的效率，并能有效地寻获并发数据结构中一些难以发现的错误。