Verified Compilation of the Modular Reset, Finally

Abstract

We present the formalization of the semantics of the modular reset construct of Lustre, and show how to integrate it into Vélus, a Lustre compiler verified in Coq and built on top of CompCert. In particular, we introduce a new intermediate language in the compilation chain, specifically designed to handle compilation of the modular reset.