The Vélus project is an ongoing and long-term effort to extend techniques for formal specification and verification in Interactive Theorem Provers to the languages, tools, and applications of Model-Based Development.
We focus specifically on dataflow synchronous languages like Lustre and Scade and we work in Coq. The main concrete result of our project is the Vélus verified Lustre compiler. This compiler can be seen as an extension of CompCert for compiling Lustre.
Embedded control software defines the interactions of specialized hardware with the physical world. It normally ticks away unnoticed inside systems like medical devices, trains, aircraft, satellites, and factories. But this software is complex and potentially serious errors are difficult to avoid, especially over many years of maintenance and reuse. Engineers have long designed such systems using block diagrams and state machines to represent the underlying mathematical models. The key idea of Model-Based Development is that such models can be executable and serve as the base for simulation, validation, and automatic code generation.
Interactive theorem provers, also sometimes called as proof assistants, are software tools for functional programming, formal specification, and machine-checked proof. Broadly speaking, our goals are to
Develop semantic models for the source language inside an interactive theorem prover.
Develop a compiler with a formal proof that the semantics of a source model are implemented by the code generated for it.
Provide tools for interactive reasoning about source models and libraries with results guaranteed down to the code that executes.
Active development is concentrated at the PARKAS research team at Inria Paris.
The following people contribute or have contributed to the project: Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Paul Jeanmaire, Xavier Leroy, Basile Pesin, Marc Pouzet, and Lionel Rieg.
The source code is available under an Inria Non-Commercial License.
Basile's thesis defense with links to the dissertation, slides, and online compiler.
Basile Pesin presents our paper Verified Compilation of Synchronous Dataflow with State Machines and poster at EMSOFT 2023 (slides). There is a table that links the main definitions and theorems from the paper to the Coq source and an online version of the extracted compiler.
Basile Pesin presented his ongoing thesis work at JFLA 2023 in Praz-sur-Arly.
Paul Jeanmaire presented his ongoing thesis work at TYPES 2022 in Nantes.
SIGBED blog post on our EMSOFT 2021 article.
Keynote on Vélus at REBLS 2021. A recording is available.
Best paper at EMSOFT 2021!
Our paper Verified Lustre normalization with node subsampling and poster will be presented next week at EMSOFT 2021 (slides). There is a table that links the main definitions and theorems from the paper to the Coq source.
Our paper on extending Vélus with normalization and node subsampling has been accepted at EMSOFT 2021.
Paul Jeanmaire joins the project as a PhD student.
Basile Pesin joins the project as a PhD student.
Lélio presented his slides at POPL 2020. A video is available.