如何正式验证编译器（前端和/或后端）？

Question

对于我即将开始的项目，我正在探索编译器的形式验证。我遇到了 CompCert C 编译器，它是 ACM 授予的、经过正式验证的 C 编译器。

当我进一步阅读时，它提到它已经使用 Coq Proof Assistant 来机械化自动验证。

问题是：如何为指令翻译创建证明/定理？步骤是什么？欢迎任何指导.

Answer 1

Xavier Leroy 于 2019/2020 年在法兰西学院开设了有关该主题的课程¹。课程本身是法语的，但这里有英文版的优秀材料：https://github.com/xavierleroy/cdf-mech-sem。特别是，文件

Imp.v

和

Compil.v

将为您提供基础知识的良好开端。

然而，直接跳入 Coq 代码可能会很棘手。如 kiner_shah 所指出的，先访问或并行访问软件基金会是一个好主意。