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 …


Verified Compilation of the Modular Reset, Finally

We present the formalization of the semantics of the modular reset construct of Lustre, and show how to integrate it into Vélus, a …


Verifying the Lustre Modular Reset

We present ongoing work on the compilation of the modular reset and its proof of correctness.

Towards a Verified Lustre Compiler With Modular Reset

We present a formalization of the semantics of the modular reset and discuss its compilation.


Vélus: Towards a Modular Reset

We present two ideas in this talk:

  1. A co-inductive based semantics formalization for normalized Lustre
  2. A formalization of the semantics …


Proving a Lustre Compiler Part 2

The compilation of block diagram languages like Lustre or Scade often use an intermediary language between the source data-flow code …