可信编译器L2C的核心翻译步骤及其设计与实现

来源：软件学报杂志2017年第5期北京时间：

作者：尚书,甘元科,石刚,王生原,董渊

单位：尚书，清华大学 计算机科学与技术系, 北京 10008411,甘元科，清华大学 计算机科学与技术系, 北京 10008402,石刚，清华大学 计算机科学与技术系, 北京 10008403,王生原，清华大学 计算机科学与技术系, 北京 10008404,董渊，清华大学 计算机科学与技术系, 北京 10008405

摘要：同步数据流语言（如Lustre）近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好“误编译”问题，近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证，取得了很大的成功，如CompCert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言，以Clight（CompCert中的C语言子集）为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.

关键词：经过验证的编译器;同步数据流语言;L2C;Coq证明辅助器;核心翻译步骤

基金资助：国家自然科学基金（90818019，61462086）；国家科技重大专项（MJ-2015-D-066）；Sino-European Laboratory of Informatics，Automation and Applied Mathematics资助项目