Towards the verified compilation of Lustre

Add to your list(s) Download to your calendar using vCal

• Timothy Bourke (Inria Paris, École Normale Supérieure)
• Friday 10 March 2017, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Paul Taylor.

Dataflow synchronous languages and their compilers are used to develop safety-critical applications, like fly-by-wire controllers in aircraft and monitoring software for power plants. A striking example is the SCADE Suite tool of ANSYS /Esterel Technologies which is DO-178B/C qualified for the aerospace and defense industries. This tool allows engineers to develop and validate systems at the level of abstract block diagrams that are automatically compiled into executable code.

Formal modelling and verification in an interactive theorem prover can potentially complement the industrial certification of such tools to give very precise definitions of language features, increased confidence in their correct compilation, and a base for verifying programs; ideally, right down to the binary code that actually executes.

We have been developing these ideas by implementing a Lustre compiler in the Coq proof assistant (Lustre is the academic basis of the Scade 6 language). In this talk, I will describe this ongoing work and detail some of our recent technical results, namely the proof of correctness for the translation to an imperative intermediate language, the integration of the CompCert C compiler, and the application of separation logic assertions to justify low-level code generation.

This is joint work with Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.