Representative: Jean-Francois Monin
Involved Lab: UMR 5104, Centre Equation, GIERES
Representative: Shengyuan Wang
Involved Lab: Laboratory of System Software and Software Engineering Software Institute, Department of Computer Science and Technology
The goal of this project is to address the application of formal methods applied to the formal certification of open-source software tools. By formal certification, we mean that these tools are formally proved correct and that the formal proof itself is checked by a reliable world-class proof-assistant such as Coq or Isabelle. In the sequel, the world formal certification (or just certification, for short), is exclusively used with this meaning. In the last decade, these proof assistants proved mature enough to attack the certification of compilers and OS components. For instance, the Compcert project at INRIA provides a formally certified C compiler: given an arbitrary (up to minor restrictions) C source code, it makes an executable machine program which behaves exactly as the source, according to formal semantics of the source and target languages.
We will also focus on approaches based on Coq.
More specifically, we want to develop various tools along similar lines: (1) a certified compiler for the Lustre language, targetting the C language, which will be combined with results from CompCert and possibly Verasco in order to get a certified chain from Lustre to machine language. (2) static checkers for some kinds of inconsistent or unsafe behaviors of key component of operating systems such as file systems, network protocol stacks and device drivers.
The main rationale for this choice is that the three partners already have a good background in the corresponding technologies (proof assistants, Lustre) and that sharing available skills and experiences will result in a much stronger team, able to develop tools and results which would remain out of reach for each partner separately.
We also hope that this partnership will make the field and our teams more attractive to promising students, including from the undergraduate and graduate level. In the long run, this should help both to consolidate this project and to improve students exchanges between our universities, in combination with more general cooperation agreements between partners.
The project is located at Tsinghua and Verimag. We will use standard tools (svn or git) for shared developments. Regular (e.g., monthly) teleconference meetings will be organized. Each partner will also send researcher to its partners and host researchers from its partners.