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

作     者：尚书 甘元科 石刚 王生原 董渊 SHANG Shu;GAN Yuan-Ke;SHI Gang;WANG Sheng-Yuan;DONG Yuan

作者机构：清华大学计算机科学与技术系北京100084 

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

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2017年第28卷第5期

页      码：1233-1246页

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

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

学科分类：08[工学] 0835[0835] 0811[工学-水利类] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.13328/j.cnki.jos.005213

馆 藏 号：203231066...