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.
翻译:2007年,利用Coq校准助理对C.等低需要语言的记忆模型进行了正式核查。 考虑到其正规化基本上是在一阶逻辑下进行的,作者留下的一个问题是,其证据能否使用一阶逻辑的核查框架实现自动化;我们接受挑战,使用Wais3将其正规化自动化,大大减少了举证努力;我们系统地遵循了Coq校准,并意识到在许多情况下,离解所有VC的途径只有三分之一左右。 此外,仍然需要互动的证据(如感应、生存证据证人、声明)被作为孤立的辅助结果,我们明确表明了这一点。通过这种方式,我们取得了记忆模型几乎自动的健全和安全证明。然而,我们的发展允许提取一个正确、按部位构建的具体记忆模型,因此比最初的Leroy和Blazy版本更进一步。