Towards the verified compilation of Lustre
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 listsWhat's on in Physics? Type the title of a new list here Cargo
Other talksRSLC PhD/Postdoc Seminar (Chemistry) Open slot Solution of an old problem in vector optimisation: Support function of the generalised Jacobian RSLC PhD/Postdoc Seminar (Chemistry) Open slot Algorithms and barriers for random instances of computational problems