Abstract
The seminar focused on the formalization and proof in Coq of an imperative code generator for a kernel of the Lustre language. Such formal verification could usefully complement the official certification methods currently employed for SCADE 6, which integrates Lustre and a restricted version of Esterel. Although the compiler core is only a small part of the total system, it is essential because any bug generated by this core can have unpredictable and potentially serious consequences.
The talk presented the specification and verification of a simple code generator that handles Lustre's main features: sampling, nodes and delays. The code generation chain integrates the formally verified CompCert C compiler to produce the final assembler code. The guarantees offered by CompCert make it possible to extend Lustre's translation correction theorem to the entire chain of compiling Lustre programs into assembler.
