一句话：将并发程序基于交错的正确性证明自动转换为 Owicki-Gries 风格线程模块化证明，并合成 ghost 变量以压缩证明。
算法软件验证器的实现缺陷会威胁其可靠性；为正确程序生成正确性证书可实现独立校验，但并发程序基于交错的正确性论证可能随交错数指数爆炸。本文提出一种方法，将许多算法验证器生成的基于交错的正确性证明转换为 Owicki 与 Gries 风格的线程模块化证明。该方法自动合成 ghost 变量，以捕获与证明相关的交错信息，同时抽象掉无关细节，从而消除对具体交错的依赖。作者在实现中评估了该方法的实践效率，并与基线比较；结果表明该方法高效且能生成紧凑的正确性证明，有助于并发程序验证结果的独立验证。
Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact correctness proofs for concurrent programs is challenging, as the correctness arguments may depend on the particular interleaving, which can lead to exponential explosion. We present an approach that converts an interleaving-based correctness proof, as generated by many algorithmic verifiers, into a thread-modular correctness proof in the style of Owicki and Gries. We automatically synthesize ghost variables that capture the relevant interleaving information, and abstract away irrelevant details. Our evaluation shows that the approach is efficient in practice and generates compact proofs, compared to a baseline.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-20369,
title = {The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs},
author = {Frank Schüssele and Matthias Zumkeller and Miriam Lagunes-Rochin and Dominik Klumpp},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776684}
}