The ``ProofInUse'' consortium is a laboratory for research and development in the domain of high-assurance software. It is joint between several academic and industrial partners. The general objective of ProofInUse is to provide software verification tools, based on mathematical proof, to industry users. These tools would be aimed at replacing or complementing the existing test activities, whilst reducing costs.
This consortium is led by the Inria project-team Toccata, and is a follow-up of the former ``LabCom ProofInUse'' funded by ANR between 2014 and 2017.
The current partners of ProofInUse are the following.
- The AdaCore company in Paris, providing development tools for the Ada programming language.
- The TrustInSoft company in Paris, providing static analysis tools for the C and C++ programming languages.
- The Mitsubishi Electric R&D Centre Europe in Rennes, conducting research and development into next generation communication & information systems and power electronic systems.
- The LSL laboratory of the CEA List in Saclay, developing methods and tools for the verification and validation of safety- and security-critical software.
- The OCamlPro company in Paris, specialized in research and development on programming languages, formal methods, blockchains as well as their application in industrial settings.
The objective of ProofInUse is thus to significantly increase the capabilities and performances of verification environments proposed or internally used by these partners. Beyond a common interest in formal verification techniques, the members of ProofInUse share a common interest in the generic environment Why3 for deductive program verification, developed in the Toccata research group. In particular, ProofInUse aims at integration of verification techniques at the state-of-the-art of academic research, via the Why3 environment.
Joining the consortium
The ProofInUse consortium is not a formal nor a legal entity. As such, the consortium is widely open to welcome new academic or industrial partners. In essence, joining to the consortium allows one to get access to the general information exchanged between, including the participation to the regular plenary meetings of the consortium. The underlying discussions and exchanges aims at identifying shared subjects of interest, which may or may not lead to new developments or improvements in the current Why3 project. Indeed, in a more practical aspect, joining the consortium includes the creation of personal accounts on the Inria gitlab, as member of the Why3 project, allowing to submit issues, create merge requests, and follow any discussions taking place on this gitlab project.For any more information and request for joining, send an e-mail to Claude Marché.
External links
- The Toccata research team
- The Why3 software environment
- The Why3-Club mailing list
- The AdaCore company
- The SPARK2014 software environment
- The former ``LabCom ProofInUse'' between Toccata and AdaCore in 2014-2017
- The TrustInSoft
company
- Online tools: TrustInSoft-CI and TSnippet online platform
- TrustInSoft Analyzer
- The Mitsubishi Electric R&D Centre-Europe in Rennes.
-
The LSL laboratory of CEA List
- The Frama-C collaborative platform dedicated to source-code analysis of C software.
- The OCamlPro company