Proof in Use

The objective of the joint laboratory 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.

ProofInUse originates from the sharing of resources and knowledge between the Toccata research team, specializing in techniques for program proofs and the SME AdaCore, a software publisher, specializing in providing software development tools for critical systems. A previous successful collaboration between Toccata and AdaCore enabled Toccata’s Why3 technology, to be put into the heart of the AdaCore-developed SPARK technology.

The purpose of the joint laboratory ProofInUse is to increase significantly the number of industrial customers of the SPARK technology, thus democratizing the use of proof techniques. This democratization requires the resolution of several scientific and technological challenges:

A first axis of research and innovation is to facilitate the use of automatic provers.

This first aspect requires the provision of a better interaction with the user, especially for debugging non-provable specifications as it is customary to expect for other development activities. Then, the joint laboratory will aim at improving the ratio of provability of programs commonly used in industry, in particular for numerical computations and data manipulations. Indeed, the economic interest of proof techniques is based largely on their automation, hence any improvement in this respect will result in the SPARK technology becoming more attractive. These two points require scientific breakthroughs in terms of support to the generation of counter-examples and modeling of data types adapted to the intrinsic capacities of automated provers.

A second axis of research and innovation is to allow the user to go beyond what is possible with the current SPARK technology, in terms of specification of programs and the proofs of these specifications.

On the specification side, it will require the support for more complex constructions in the Why3 technology, permitting the extension of the programming language included in SPARK. This will, in particular, satisfy the user’s need to specify data invariants. On the proof side, the objective of the joint laboratory is to give the user the possibility to guide the proof for more complex properties - for instance, those resistant to automated provers. These two points require scientific advances not only at the level of the intermediate language constructs used for proofs, but also in the methods for generating proof obligations, permitting these uses.

 

Sponsors

AdaCore Altran CNRS Inria