Project aims to grow use of mathematical proof-based software verification tools

Project aims to grow use of mathematical proof-based software verification tools

Technology News |
By eeNews Europe

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.

“We live in a world that is increasingly run by software, meaning that it is vital that programs are highly reliable, safe and secure,” says Cyrille Comar , president at AdaCore. “Developing the proof-based techniques used within SPARK and making sure that they are fully integrated with others verification techniques such as testing is a major step to reducing testing costs and time, while ensuring that safety requirements are met. The public/private collaboration within ProofInUse will provide the impetus to help spread proof-based techniques and thus increase adoption, benefiting both industry and the wider public.”

AdaCore provides commercial software solutions for Ada, the programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore’s flagship product is the open source GNAT Pro development environment; the company sees Ada and GNAT Pro gaining usage in high-integrity and safety-certified applications, including space-based systems, commercial aircraft avionics, military systems, air traffic management/control, rail systems, and medical devices, and in security-sensitive domains, such as financial services. AdaCore offers the SPARK Pro toolset for these contexts.

If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :    eeNews on Google News


Linked Articles