Publications

Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development …

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 …

A Formally Verified Compiler for Lustre

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are …