Contact

The objective of ProofInUse is to provide 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 laboratory is a joint effort of the Inria project-team Toccata, the The AdaCore company which provides development tools for the Ada programming language, and the TrustInSoft company which provides static analysis tools for the C and C++ programming language.

The objective of ProofInUse is thus the significantly increase the capabilities and performances of verification environments proposed by these two companies. It aims at integration of verification techniques at the state-of-the-art of academic research, via the generic environment Why3 for deductive program verification developed by Toccata.

This joint laboratory is a follow-up of the former ``LabCom ProofInUse'' funded by ANR.

Meetings

Publications