论文标题
Leroy和Blazy是正确的：他们的内存模型声音证明是可自动的（扩展版本）
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
论文作者
论文摘要
2007年，Xavier Leroy和Sandrine Blazy使用COQ证明助手进行了正式的验证，该模型是针对C.等低水平命令语言的记忆模型，例如C.考虑其形式化基本上是在一阶逻辑中进行的，作者留下的一个问题是，作者是否可以使用一阶逻辑进行证明，是否可以自动化证明。我们采取了挑战，并使用Why3自动化了他们的形式化，从而大大减少了证明工作。我们系统地遵循了COQ证明，并意识到，在许多情况下，3为什么3可以卸下所有VC。此外，仍然需要相互作用的证据（例如，归纳，存在证明的证人，断言）是分解了我们明确指出的辅助结果。这样，我们实现了记忆模型几乎自动的健全性和安全性证明。尽管如此，我们的开发允许提取正确的构造混凝土内存模型，因此，与leroy和blazy版本的初步版本相比，它更进一步。
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering their formalization was performed essentially in first-order logic, one question left open by the authors was whether their proofs could be automated using a verification framework for first-order logic. We took the challenge and automated their formalization using Why3, significantly reducing the proof effort. We systematically followed the Coq proofs and realized that in many cases at around one third of the way Why3 was able to discharge all VCs. Furthermore, the proofs still requiring interactions (e.g. induction, witnesses for existential proofs, assertions) were factorized isolating auxiliary results that we stated explicitly. In this way, we achieved an almost-automatic soundness and safety proof of the memory model. Nonetheless, our development allows an extraction of a correct-by-construction concrete memory model, going thus further than the preliminary Why version of Leroy and Blazy.
