Key Translations of the Trustworthy Compiler L2C and Its Design and Implementation
Author:
Affiliation:

Clc Number:

Fund Project:

National Natural Science Foundation of China (90818019, 61462086); National Science and Technology Major Project (MJ-2015-D-066); Sino-European Laboratory of Informatics, Automation and Applied Mathematics Grants

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    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.

    Reference
    Related
    Cited by
Get Citation

尚书,甘元科,石刚,王生原,董渊.可信编译器L2C的核心翻译步骤及其设计与实现.软件学报,2017,28(5):1233-1246

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 15,2016
  • Revised:September 25,2016
  • Adopted:
  • Online: January 22,2017
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063