使用验证重写引擎加速验证编译器的开发
摘要：编译器是形式验证的主要目标，因为编译器的错误会影响高层次的正确性保证，但如果必须提供证明修补程序，编译器的改变可能会变得更加费时费力。一种吸引人的方法是将编译器表现为代数重写规则的集合，一个通用引擎可以有效地应用。现在每个重写规则都可以单独证明，无需重新审查其他部分编译器的过去证明。我们以Coq证明助手为基础，提出了这一思想的首个实现。我们的新Coq命令将正常已证明的定理自动组合成具有证明的快速编译器。我们将这一框架应用于改进Fiat Cryptography工具链，用于生成密码算术，生成了一个提取的命令行编译器，速度提高了1000倍，同时具有更简单的编译器特定证明。
作者：Jason Gross and Andres Erbsen and Jade Philipoom and Miraya Poddar-Agrawal and Adam Chlipala
论文ID：2205.00862
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-07-19