Formal Verification of Compiler Algorithms

因为编译器是几乎所有计算机系统的可信组件，所以对其正确性有可信的证明是很重要的。近年来发展了一种利用高阶抽象汇编语言验证编译器正确性的新方法。本项目旨在研究如何将这些证明扩展到更现实的编译器中。证明过程的机械支持将通过提供对人类证明者工作的独立验证，使结果证明更加可信。本项目活动的三个主要领域包括：(1)使用机械定理证明器来支持编译器正确性证明，(2)将此类证明扩展到优化编译器，以及(3)合作开发用于Scheme的经过验证的编译器。

Because compilers are trusted components of almost every computer system, it is important to have trustworthy proofs of their correctness. A new method of proving compilers correct using higher- order abstract assembly language has been developed recently. This project is to study how to extend such proofs to more realistic compilers. Mechanical support for the proof process will allow the resulting proofs to be more trustworthy by supplying independent verification of the human prover's work. Three main areas of activities in this project include: (1) the use of mechanical theorem- provers to support compiler correctness proofs, (2) the extension of such proofs to optimizing compilers, and (3) a cooperative development of a verified compiler for Scheme.