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
Postdoctoral research scientist in Computer Science
My research interests include synchronous languages, functional programming and verified compilation.