Abstract
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.
Publication
Proceedings of the 21st International Workshop on Software and Compilers for Embedded SystemsSCOPES'18
Lelio Brun
Postdoctoral research scientist in Computer Science
My research interests include synchronous languages, functional programming and verified compilation.