Automatically verified code generation from Lustre code

What is it about?

We tackle the challenge of the generation of correct C code from the modeling language Lustre. We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that external solvers discharge.

Featured Image

Photo by S. Tsuchiya on Unsplash

Photo by S. Tsuchiya on Unsplash

Why is it important?

Lustre is a synchronous language used as an intermediate language in Model-Based Design tools such as SCADE Suite. Those industrial tools are used to model critical applications running on embedded systems like aircraft controls, automated train systems, or power plant monitoring software. Generating correct code from models of critical applications is crucial.