![]() |
![]() |
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 listsSeminars on Advanced Materials Combinatorics and Probability seminar Postgraduate Seminars in the School of Computer ScienceOther talksSignatures of structural criticality and universality in the cellular anatomy of the brain Topological magnons and quantum magnetism Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Many-body localization from Hilbert- and real-space points of view The percolating cluster is invisible to image recognition with deep learning [Friday seminar]: Irradiated brown dwarfs in the desert |