Towards a Verified Lustre Compiler with Modular Reset

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 Systems
SCOPES’18
Avatar
Lélio Brun
PhD candidate in Computer Science

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

Related