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.
Model-Based Development
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
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.
The Team
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.
Source Code
The source code is available under an Inria Non-Commercial License.
News
- 2022-06-21
Paul Jeanmaire presented his ongoing thesis work at TYPES 2022 in Nantes.
- 2022-04-12
SIGBED blog post on our EMSOFT 2021 article.
- 2021-10-18
Keynote on Vélus at REBLS 2021. A recording is available.
- 2021-10-12
Best paper at EMSOFT 2021!
- 2021-10-04
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.
- 2021-07-06
Our paper on extending Vélus with normalization and node subsampling has been accepted at EMSOFT 2021.
- 2020-10-01
Paul Jeanmaire joins the project as a PhD student.
- 2020-09-01
Basile Pesin joins the project as a PhD student.
- 2020-07-06
- 2020-01-24
Lélio presented his slides at POPL 2020. A video is available.
- 2019-10-11
Our paper on extending Vélus with a reset operator has been accepted at POPL 2020.
- 2019-09-02
Postdoc and PhD positions in the Vélus project are now open on Inria's recruitment website.
- 2019-07-12
The ANR (French national funding agency) will fund the FidelR, Fidelity in Reactive Systems Design and Compilation, JCJC project. The goal is to add state machines to the Vélus compiler and develop techniques for interactive verification of Lustre programs. Anyone wanting to do a post doc or PhD in these topics should contact us.
- 2019-07-01
Creation of the Vélus website.