Titre : Verifying clock-directed modular code generation for Lustre Auteur : Pierre-Evariste Dagand Abstract : This work addresses the compilation pass that transforms synchronous dataflow programs into imperative programs. The challenge is to move from a dataflow semantics, where programs manipulate streams of values, to an imperative one, where programs perform stateful computations. We specify and verify in the Coq interactive theorem prover a code generator that handles the key aspects of Lustre including nodes and delays. This is joint work with Timothy Bourke, Marc Pouzet and Lionel Rieg.