ProofInUse: a joint Inria and AdaCore laboratory
Date:
Publish on 29/01/2020
Claude Marché, Toccata team leader - © Inria / Photo Kaksonen
With the launch of a joint laboratory, the Toccata research team, which specialises in formal specification and computer-assisted proofs, is increasing its collaboration with AdaCore, the specialist publisher of development software for critical systems.
With the launch of a joint laboratory, the Toccata research team, which specialises in formal specification and computer-assisted proofs, is increasing its collaboration with AdaCore, the specialist publisher of development software for critical systems.
In January 2014, the French National Research Agency (ANR) gave its go-ahead for the creation of "ProofInUse", the laboratory created jointly by Toccata, an Inria team specialising in formal specification and computer-assisted proofs, and the software publisher AdaCore. At the same time, the joint laboratory will receive funding for three years, which will enable the two partners to perfect the technologies they are developing to support businesses. This latest step in the collaboration between Toccata and AdaCore is intended to offer industry a system for checking the computer code in their software. Based on the technique of mathematical proofs, the method aims to replace or supplement existing testing activities while reducing testing costs. Several scientific and technological hurdles need to be overcome, however, before any widespread roll-out of this method. The two partners intend to popularise the SPARK/Why3 toolkit with industry under this joint laboratory arrangement. "The funding granted by the National Research Agency enables us to recruit two high-level R&D post-grads," explains Claude Marché, Toccata team leader. "All the joint lab participants will be in touch with customers of the SPARK proofing technology."
Popularising the use of proofing techniques
The unit makes no secret of its aims."A first area of research will consist of making automatic provers easier to use by providing a more functional interface,"explains YannickMoy, a developer for AdaCore. "The joint lab will then target improving the provability ratio of programs commonly used in industry, especially for digital computation and data manipulation."
The joint laboratory will also aim to improve the capacity of these systems. They will consequently be more effective, especially in complex situations where automatic provers cannot run.
Toccata and AdaCore have previously worked together on the Hi-Lite project, which made it possible to integrate the Why3 toolbox developed by Toccata into the SPARK software developed by AdaCore. This joint effort brought about a definite improvement in the performance of verification sequences and a reduction in the risk of error during the development of embedded software. In addition, a CIFRE (research-based training scheme) PhD, funded by publisher AdaCore, is currently supervised by Toccata. "AdaCore's recruitment of two former PhD students from our team has strengthened our connection further," Claude Marché explains. "On the AdaCore side, they are very active in promoting the Toccata team's proofing approaches."