一句话：提出动态-符号运行时验证技术，通过对称破缺谓词与 epoch 分解降低 MPI 程序验证的复杂度。
消息传递并发中的通信非确定性是 MPI 程序验证难以处理的主要原因。许多实际程序具有对称的通信结构并按 epoch 分解以获取效率，因此可利用对称性与 epoch 结构降低验证复杂度。本文针对单路径 MPI 程序提出一种动态-符号运行时验证技术：一方面通过指定对称破缺谓词（SBP）利用通信对称性，阻止符号判定过程探索搜索空间中的同构部分；另一方面基于 epoch 进行组合式验证，限制某一时刻需要分析的程序规模。作者证明了该分析在给定输入下对单路径 MPI 程序是可靠且完备的。原型工具 SIMIAN 的实验表明，与先前的 trace 验证器相比，该方法显著缩短了验证时间，并能扩展到更大的基准规模。
Communication nondeterminism is one of the main reasons for the intractability of verification of message passing concurrency. In many practical message passing programs, the non-deterministic communication structure is symmetric and decomposed into epochs to obtain efficiency. Thus, symmetries and epoch structure can be exploited to reduce verification complexity. In this paper, we present a dynamic-symbolic runtime verification technique for single-path MPI programs, which (i) exploits communication symmetries by way of specifying symmetry breaking predicates (SBP) and (ii) performs compositional verification based on epochs. On the one hand, SBPs prevent the symbolic decision procedure from exploring isomorphic parts of the search space, and on the other hand, epochs restrict the size of a program needed to be analyzed at a point in time. We show that our analysis is sound and complete for single-path MPI programs on a given input. Using our prototype tool SIMIAN, we further demonstrate that our approach leads to (i) a significant reduction in verification times and (ii) scaling up to larger benchmark sizes compared to prior trace verifiers.