A formally verified transformation to unify multiple nested clocks for a Lustre-like language

作     者：Gang SHI Yucheng ZHANG Shu SHANG Shengyuan WANG Yuan DONG Pen-Chung YEW 

作者机构：Department of Computer Science and Technology Tsinghua University Department of Computer Science and Engineering University of Minnesota 

出 版 物：《Science China(Information Sciences)》 (中国科学:信息科学(英文版))

年 卷 期：2019年第62卷第1期

页      面：208-210页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 61272086, 61462086, MJ-2015-D-066) SinoEuropean Laboratory of Informatics, Automation and Applied Mathematics (Grants for the project Formally Certified Software Tools) 

主　　题：A formally verified transformation to unify multiple nested clocks for a Lustre-like language cycle 

摘      要：Multiple nested clocks is a major language feature in synchronous data-flow languages such as Lustre [1]. To build a formally verified compiler for such a language, it is a common practice to compile the source program to a C-like program first before compiling it to low-level machine-dependent code using a formally verified backend compiler