Leroy 与 Blazy 是正确的：其内存模型可靠性证明可自动化（扩展版）
计算机科学中的逻辑
2022-12-06 v1 编程语言
摘要
Xavier Leroy 与 Sandrine Blazy 于 2007 年使用 Coq 证明助手对 C 等低级命令式语言的内存模型进行了形式化验证。考虑到他们的形式化本质上是在一阶逻辑中完成的，作者留下的一个开放问题是：其证明能否使用一阶逻辑的验证框架实现自动化。我们接受了这一挑战，并使用 Why3 将其形式化自动化，显著减少了证明工作量。我们系统地遵循了 Coq 证明，并意识到在许多情况下，约在三分之一处 Why3 便能 discharge 所有验证条件（VCs）。此外，仍需要交互的证明（如归纳、存在性证明的见证、断言）被因式分解，隔离出我们显式陈述的辅助结果。以此方式，我们实现了内存模型几乎自动的可靠性与安全性证明。尽管如此，我们的开发允许提取一个构造即正确的具体内存模型，从而超越了 Leroy 与 Blazy 初步的 Why 版本。
引用
@article{arxiv.2212.02425,
title = {Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)},
author = {Pedro Barroso and Mário Pereira and António Ravara},
journal= {arXiv preprint arXiv:2212.02425},
year = {2022}
}
备注
To be published in VSTTE'22