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

作者：Shi, Gang^*; Zhang, Yucheng; Shang, Shu; Wang, Shengyuan^*; Dong, Yuan; Yew, Pen Chung^*

来源：Science China Information Sciences, 2019, 62(1): 012801.

DOI：10.1007/s11432-016-9270-0

<正>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

• 出版日期2019-1
• 单位清华大学