Synchronous Languages

Towards a Verified Lustre Compiler with Modular Reset
This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal …
PDF Project Slides DOI
A Formally Verified Compiler for Lustre
The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are …
PDF Project Slides Video DOI