![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Towards the verified compilation of Lustre
Towards the verified compilation of LustreAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsContemporary History Seminar Metamaterials and Nanophotonics Group Seminars Postgraduate Seminars in the School of Computer ScienceOther talksHorizontal Mean Curvature Flow and stochastic optimal controls TBA Hunt for an Earth-twin The tragic destiny of Mileva Marić Einstein Quantum Sensing in Space TBA |