SCIENCE CHINA Information Sciences, Volume 62 , Issue 1 : 012801(2019) https://doi.org/10.1007/s11432-016-9270-0

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

More info
  • ReceivedJun 29, 2017
  • AcceptedSep 6, 2017
  • PublishedJun 27, 2018


There is no abstract available for this article.


[1] Halbwachs N, Caspi P, Raymond P. The synchronous data flow programming language LUSTRE. Proc IEEE, 1991, 79: 1305-1320 CrossRef Google Scholar

[2] Leroy X. Formal verification of a realistic compiler. Commun ACM, 2009, 52: 107-115 CrossRef Google Scholar

[3] Bourke T, Brun L, Dagand P, et al. A formally verified compiler for Lustre. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelona, 2017. 586--601. Google Scholar

[4] Jahier E, Raymond P, Haibwachs N. The Lustre V6 Reference Manual. Software Version: master.737 (27-04-18), 2018. Google Scholar