一句话：提出基于程序上下文的两类可靠程序归约，利用步骤可交换性简化并发程序安全性证明与自动验证。
并发与分布式程序的正确性推理通常依赖程序归约来简化。本文提出一种通过探索通用归约类来自动简化并发程序证明的方法，引入两类可靠（sound）的程序归约，分析其理论性质，并展示如何用于算法化验证。核心创新是在归约定义中引入“上下文”概念：利用程序步骤在某些上下文中的可交换性定义通用可靠归约，从而无需针对特定语法特征即可自动生成证明。案例表明，该方法能有效处理多样程序，并为当前自动验证技术理论上难以获得完整 Floyd–Hoare 风格证明的程序生成证明。
Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic classes of reductions. We introduce two classes of sound program reductions, study their theoretical properties, show how they can be effectively used in algorithmic verification, and demonstrate that they are very effective in producing proofs of a diverse class of programs without targeting specific syntactic properties of these programs. The most novel contribution of this paper is the introduction of the concept of context in the definition of program reductions. We demonstrate how commutativity of program steps in some program contexts can be used to define a generic class of sound reductions which can be used to automatically produce proofs for programs whose complete Floyd-Hoare style proofs are theoretically beyond the reach of automated verification technology of today.