Formal Verification of Compiler Algorithms

编译器算法的形式验证

• 批准号: 9014603
• 负责人: Mitchell Wand
• 金额: --
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-07-01 至 1994-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9014603&HistoricalAwards=false
• 关键词: Formal; Verification; Compiler; Algorithms

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.

因为编译器是几乎每台计算机的可信组件 系统，重要的是要有可信的证据， 正确性 一种用高级语言证明编译器正确性的新方法 顺序抽象汇编语言是近年来发展起来的。 这 项目是研究如何将这种证明扩展到更现实的 编译器。 机械支持的证明过程将允许 通过提供独立的证明， 验证人类的工作。 的三个主要领域 该项目的活动包括：（1）使用力学定理- 支持编译器正确性证明的证明器，（2）扩展 这种证明对优化编译器，和（3）合作开发 一个经过验证的Scheme编译器