ProofInUse Initiative Launched, Will Deliver Verification Tools for Critical Systems
Public/private laboratory for mathematical proof-based tools led by Inria and AdaCore
Paris, 2 February 2015, A major new partnership launched today aims to increase the use of mathematical-proof based verification tools within the software industry. ProofInUse, a joint laboratory led by Inria, a computational science research institute, and AdaCore, the leading provider of commercial software solutions for the Ada language, aims to spread the adoption of proof-based tools, replacing or complementing existing activities while reducing software development and verification costs.
Funded by the French government, the common laboratory is being launched at a kickoff conference held today 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). 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.
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,” 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.”
About Inria
Established in 1967, Inria is the only public research body fully dedicated to computational sciences. Combining computer sciences with mathematics, Inria’s 3,500 researchers strive to invent the digital technologies of the future. Educated at leading international universities, they creatively integrate basic research with applied research and dedicate themselves to solving real problems, collaborating with the main players in public and private research in France and abroad.
Inria contributes to innovation within France by transferring its technologies and skills to industry. Inria has a range of schemes to promote technology transfer, including a programme specifically aimed at SMEs, strategic partnerships with R&D departments of major industrial groups, and support for business start-ups. A team of professionals is on hand to support researchers and entrepreneurs in the development of their value-added projects. Inria is celebrating 30 years of business creation, the opportunity to remind ourselves that the creation of businesses is one of the areas Inria decided to focus on in its search for economic and societal impact.
The researchers at Inria published over 4,450 articles in 2012. They are behind over 250 active patents and 112 start-ups. The 180 project teams are distributed in eight research centers located throughout France. www.inria.fr
About AdaCore
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical, and security-critical systems.
Four flagship products highlight the company’s offerings:
- The GNAT Pro development environment for Ada, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability,
- The CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software,
- The SPARK Pro verification environment, a toolset based on formal methods and oriented towards high-assurance systems, and
- The QGen model-based development tool, a qualifiable and customizable code generator and verifier for SimulinkÆ and StateflowÆ models, intended for safety-critical control systems.
Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as space systems, commercial avionics, military systems, air traffic management/control, rail systems, medical devices, and financial services. AdaCore has an extensive and growing world-wide customer base; see www.adacore.com/customers/ for further information.
AdaCore products are open source and come with expert on-line support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com