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

摘要：

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

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

所属期刊栏目：28

分类号：TP314(计算技术、计算机技术)

资助基金：国家自然科学基金90818019,61462086;国家科技重大专项MJ-2015-D-066;Sino-European Laboratory of Informatics,Automation and Applied Mathematics资助项目 National Natural Science Foundation of China90818019,61462086;National Science and Technology Major ProjectMJ-2015-D-066;Sino-European Laboratory of Informatics,Automation and Applied Mathematics Grants

在线出版日期：2017-06-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共14页

页码：1233-1246