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

• 作者: 尚书 王生原 甘元科 石刚 董渊
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 经过验证的编译器 同步数据流语言 L2C Coq证明辅助器 核心翻译步骤
• 年，卷（期）: 2017,（5）
• 所属期刊栏目: 形式化方法与应用专题
• 页码范围: 1233-1246
• 页数: 14页
• 分类号: TP314
• 字数: 11358字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005213

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
2	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
3	石刚	清华大学计算机科学与技术系	11	38	4.0	5.0
4	甘元科	清华大学计算机科学与技术系	5	24	4.0	4.0
5	尚书	清华大学计算机科学与技术系	1	8	1.0	1.0