主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
尚书,甘元科,石刚,王生原,董渊.可信编译器L2C的核心翻译步骤及其设计与实现.软件学报,2017,28(5):1233-1246
可信编译器L2C的核心翻译步骤及其设计与实现
Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation
投稿时间:2016-07-15  修订日期:2016-09-25
DOI:10.13328/j.cnki.jos.005213
中文关键词:  经过验证的编译器  同步数据流语言  L2C  Coq证明辅助器  核心翻译步骤
英文关键词:certified compiler  synchronous data-flow language  L2C  Coq proof assistant  key translation
基金项目:国家自然科学基金(90818019,61462086);国家科技重大专项(MJ-2015-D-066);Sino-European Laboratory of Informatics,Automation and Applied Mathematics资助项目
作者单位E-mail
尚书 清华大学 计算机科学与技术系, 北京 100084 shangs14@mails.tsinghua.edu.cn 
甘元科 清华大学 计算机科学与技术系, 北京 100084  
石刚 清华大学 计算机科学与技术系, 北京 100084  
王生原 清华大学 计算机科学与技术系, 北京 100084  
董渊 清华大学 计算机科学与技术系, 北京 100084  
摘要点击次数: 1334
全文下载次数: 990
中文摘要:
      同步数据流语言(如Lustre)近年来在航空、高铁、核电等安全攸关领域得到广泛应用.这些领域对相关开发工具本身的安全性有着相当高的要求.为尽力解决好“误编译”问题,近期人们借助reliable-by-construction辅助定理证明器实现常规命令式语言编译器的构造和验证,取得了很大的成功,如CompCert C编译器.L2C是基于这种方法开发的可信编译器.它以扩展的Lustre语言为源语言,以Clight(CompCert中的C语言子集)为目标语言.L2C是面向实际工业应用的同步数据流语言编译器.重点介绍L2C编译器的核心翻译步骤及其设计与实现过程中考虑的主要问题和相关经验.
英文摘要:
      Synchronous data-flow languages, such as Lustre, have been widely used in safety-critical industrial areas, such as airplanes, high-speed railways, and nuclear power plants. The safety of development tools themselves for these types of applications is highly required. In better solving the "miscompilation" problem, very successful progress has been made recently to implement the construction and verification of a conventional imperative language compiler, such as the CompCert C compiler, by using reliable-by-construction proof assistants. L2C is a trustworthy compiler developed based on such an approach, with an extended Lustre language as its source, and Clight, a C subset used in ComperCert, as its target. L2C is an industry-level synchronous data-flow language compiler developed by using the same technique. The paper focuses on the key translations of L2C and the main issues and experience in its design and implementation.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利