论文标题
COMPCERT验证的编译器的可信计算基础
The Trusted Computing Base of the CompCert Verified Compiler
论文作者
论文摘要
COMPCERT是第一个现实的正式验证编译器：它提供了由机器检查的数学证明，其生成的代码与源代码匹配。然而，这种方法可能存在漏洞。我们全面分析了CompCert的各个方面，其中错误可能导致不正确的代码生成。可能的问题范围从源和目标语言的建模到用于调用编译器内部算法的某些技术。
CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.
