University of Birmingham > Talks@bham > Theoretical computer science seminar > Towards the verified compilation of Lustre

Towards the verified compilation of Lustre

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.