许多程序验证问题都可以被归结为精化验证,即证明一个较具体的程序不会比一个较抽象的程序产生更多的行为。本文发掘了在并发环境下精化验证的应用场景,并提出若干种可以支持这些精化应用实例的验证技术。具体来说,本文在理解和验证并发程序精化方面做出了如下贡献。首先,本文提出了一种基于依赖/保证的模拟关系RGSim,作为并发程序精化的通用验证手段。这一新颖的模拟关系将线程和并发环境之间的交互作为参数,从而获得可组合性,支持模块化验证。同时,它将精化应用中对并发环境的特定前提参数化,因而具有较好的灵活性和实用性。我们应用RGSim验证了并发环境下的几种程序优化。此外,我们还将并发垃圾收集器的验证归结为精化验证,并提出一种基于RGSim的通用验证框架。使用这一框架,我们验证了Boehm等人提出的并发的标记-清扫垃圾收集算法。其次,本文提出了一种霍尔风格的程序逻辑,用于高效地、模块化地验证并发对象的线性一致性。这是并发程序精化验证的一种重要应用。作为该程序逻辑的一部分,我们提出了一种轻量的辅助代码插桩机制。我们的程序逻辑支持可线性化点不固定的并发算法,这些算法的验证难度很大。具体包括：使用帮助机制的无锁算法(如HSY栈),可线性化点依赖未来不确定执行的算法(如懒惰集合算法),以及同时有这两种特性的算法(如RDCSS算法)。我们还扩展了模拟关系RGSim以支持可线性化点不固定的程序,新的模拟关系保证了我们的程序逻辑的可靠性,它可以蕴涵一种上下文精化关系,该精化关系与线性一致性等价。我们应用这一程序逻辑验证了12个著名的并发算法,其中两个算法已经在Java并发包java.util.concurrent中使用。最后,本文展示了一个用精化关系刻画并发对象完整正确性(包括线性一致性以及各种进展性性质)的统一框架。我们证明了对于满足线性一致性的并发对象,每种进展性性质等价于一种特定的对终止性敏感的上下文精化关系。我们用上下文精化关系统一了并发对象的线性一致性和所有常见的进展性性质,包括无等待性、无锁性、无阻碍性、无饥饿性和无死锁性。根据这一结果,对于任何使用并发对象操作的客户端程序,我们可以模块化地验证该客户端程序的安全性和终止性。另一方面,它也告诉我们,有希望借鉴已有的验证上下文精化的技术来同时验证线性一致性和进展性性质。