ProofInUse : kickoff meeting
After several months in construction, the ProofInUse joint laboratory is now fully operational. Today marked the official launch of work on development aimed at providing a range of verification tools for critical systems.
Jointly funded by the public and private sectors, the new laboratory has been established in order to develop verification tools using formal mathematical methods. Partly financed by the French government, and managed jointly by Inria and AdaCore, the leading supplier of software solutions for the Ada programming language, the mission of ProofInUse is to expand the use of tools based on formal methods. These tools complement or replace existing methods of software development, while at the same time reducing verification costs. The establishment of the ProofinUse joint laboratory reflects one of the priorities of the Inria Saclay - Île-de-France Centre; the safety, security and reliability of computer architectures, software and data.
The deployment of formal verification tools in industrial and software development projects enhances the automation of the verification process, reducing the costs of critical software and the associated development time. ProofInUse is based on the SPARK critical application development technology developed by AdaCore and Altran. ProofInUse will provide a research laboratory dedicated to meeting the technological and scientific associated with system verification techniques. Research will be targeted on facilitating the use of automatic demonstrators and expanding the capabilities of SPARK in verifying more complex properties.
“Verification tools based on mathematic proof have already been developed in the academic world. They have proved their worth in finding bugs in complex critical software”,explains Claude Marché, Inria Director of Research,“our collaboration with AdaCore will enable ProofInUse to continue development of these techniques, extending their use even further into the traditional software development process, and ensuring that they can be applied successfully in an industrial environment”.
ProofInUse has been created by sharing the resources and expertise of AdaCore and the Toccata research team, specialising in software verification techniques. In an earlier collaboration between AdaCore and Toccata, the Why3 technology developed by Toccata was integrated into the SPARK technology developed by AdaCore.
“We live in a world which is increasingly reliant on software, and it is essential that this software is reliable, safe and secure”,comments Cyrille Comar, CEO of AdaCore,“developing techniques based on formal methods in SPARK while ensuring that they are fully integrated with other verification techniques such as testing, constitutes a major advance in reducing the costs of software verification without compromising safety.The public / private collaboration at the heart of ProofInUse will give a new impetus to the drive to expand the use of verification techniques based on formal methods. Extending these techniques into an industrial environment can only benefit manufacturers and the wider public as a whole”.