ProofInUse aims to spread the adoption of proof-based tools, replacing or complementing existing activities while reducing software development and verification costs.
Deploying proof techniques within commercial software development, according to those promoting the initiative, enables increased automation of verification, reducing the cost and time of creating safety-critical code. Based on AdaCore’s and Altran’s existing SPARK high-reliability application development technology, ProofInUse will provide a laboratory for research into proof techniques, developing them further to meet scientific and technological challenges. In particular it will look at making it easier to use automated provers and to extend the capabilities of SPARK to support more complex properties.
Funded by the French government, the launch of the common laboratory included contributions from Inria, AdaCore, New York University, the University of Oxford, OCamIPro and CEA (French Alternative Energies and Atomic Energy Commission). As well as Inria and AdaCore, sponsors of the laboratory include Altran, ANR (French National Research Agency), CNRS (French National Center for Scientific Research) and the Université Paris Sud. This LabCom ProofInUse is fully in line with one of the research priorities of Inria’s research center at Saclay – Ile-de-France : Safety, security and reliability for architectures, softwares and data.
“Verification tools based on mathematical proof have previously been developed within the academic sector, and have shown real promise in providing high assurance when developing safety-critical software,” says Claude Marché, Senior Scientist (Directeur de Recherche) at Inria. “Through our joint work, ProofInUse will take this a step further, develop these techniques, integrate them in more traditional software development processes, to ensure they can be successfully applied within industrial applications.”
ProofInUse arose from the sharing of resources and knowledge between AdaCore and the Toccata research team, which specialises in techniques for program proofs. A previous successful collaboration enabled Toccata’s Why3 technology to be integrated into the AdaCore-developed SPARK technology.