Global Sources
EE Times-India
EE Times-India > EDA/IP

Common lab delivers proof-based tools for critical systems

Posted: 03 Feb 2015     Print Version  Bookmark and Share

Keywords:proof-based tools  software  application development  verification tools 

AdaCore, provider of commercial software solutions for the Ada language, and computational science research institute Inria teamed up to initiate ProofInUse, a joint laboratory that aims to spread the adoption of mathematical proof-based verification tools within the software industry. The move will hopefully replace or complement existing test activities while reducing software development and verification costs.

Funded by the French government, the common laboratory is being launched at a kickoff conference in Paris. It features speakers from Inria, AdaCore, New York University, the University of Oxford, OCamIPro and CEA (French Alternative Energies and Atomic Energy Commission). Apart from Inria and AdaCore, sponsors of the laboratory include Altran, ANR (French National Research Agency), CNRS (French National Centre 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 centre at Saclay – Ile-de-France: Safety, security and reliability for architectures, software and data.

Deploying proof techniques within commercial software development enables the 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.

"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," said 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," said 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."

Comment on "Common lab delivers proof-based tool..."
*  You can enter [0] more charecters.
*Verify code:


Visit Asia Webinars to learn about the latest in technology and get practical design tips.


Go to top             Connect on Facebook      Follow us on Twitter      Follow us on Orkut

Back to Top