Credible Compilation
Credible Compilation
复制标题
可信的编译
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
M. Rinard
中科院分区：
文献类型：
--
作者：
M. Rinard
本文提出了一种编译器正确性的方法，即编译器生成一个证明，证明转换后的程序正确地实现了输入程序。然后，一个简单的校验器就可以验证程序是否被正确编译。我们称产生这种证明的编译器为可信的编译器，因为它产生可验证的证据，证明它是正确运行的。
This paper presents an approach to compiler correctness in which the compiler generates a proof that the transformed program correctly implements the input program. A simple proof checker can then verify that the program was compiled correctly. We call a compiler that produces such proofs a credible compiler, because it produces verifiable evidence that it is operating correctly.