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.