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.

翻译：实现缺陷威胁着算法软件验证器的可靠性。为正确程序生成正确性证书能够实现对验证结果的高效独立验证，从而有助于揭示此类缺陷。为并发程序自动生成小型、紧凑的正确性证明具有挑战性，因为正确性论证可能依赖于特定的交错执行模式，这可能导致指数级爆炸。本文提出一种方法，可将许多算法验证器生成的交错式正确性证明，转换为Owicki-Gries风格的线程模块化正确性证明。我们自动合成能够捕获相关交错信息的幽灵变量，并抽象掉无关细节。评估结果表明，相较于基线方法，本方法在实践中具有高效性，并能生成紧凑的证明。