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 specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.

Proceedings of the 21st International Workshop on Software and Compilers for Embedded Systems
Lélio Brun
Lélio Brun
Postdoctoral research scientist in Computer Science

My research interests include synchronous languages, functional programming and verified compilation.