LabCom ProofInUse : AdaCore & Toccata team-project
In 2014, Inria and the company AdaCore launched a joint laboratory (LabCom) called ProofInUse for a duration of three years. The purpose of this joint laboratory was to propose mathematical proof-based verification tools to industry, which aim to replace or complement the activities of existing tests whilst reducing verification costs.
ProofInUse resulted from the sharing of resources and knowledge between the Toccata research team, specialised in program proof techniques, and the SME AdaCore, a software publisher specialised in the supply of development tools for critical systems. A previous successful collaborative experience between Toccata and AdaCore had enabled the Why3 technology developed by Toccata to takes its place at the heart of the SPARK technology developed by AdaCore.
- The company
Created in 1996, AdaCore is an independent French open source software publishing company. Initially focusing on the Ada development environment market, AdaCore expanded its activity to the supply of development tools for critical embedded applications. As a result it added formal proof ( SPARK , in partnership with Altran and Inria), static analysis (CodePeer) and model-based development tools (QGen) to the Ada development tools (GNAT Pro) comprising its core business. AdaCore's client base includes most of the major names in the aeronautics, space, defence, air traffic control and rail transport industries. With its American subsidiary Ada Core Technologies Inc., it has an overall turnover of approximately 20 million Euros with around 100 employees.
- The Inria team
The Inria project team Toccata is a joint team between Inria-Saclay and the Laboratory for Computer Science (UMR (joint research unit) Paris-Sud University and CNRS), whose objective is to develop methods and tools for verification, with particular emphasis on formal proofs. Toccata's research activities are divided into four areas: deductive verification of programs, automated demonstration, verification of digital programs and certification of tools. The ProofInUse LabCom mainly concerns the first of these areas, in particular work around the development of the Why3 software.
- Purpose of the laboratory
The aim of the ProofInUse LabCom was to propose mathematical proof-based verification tools to industry, in order to replace or complement the activities of existing tests whilst reducing verification costs. The goal was to significantly increase the number of industry clients of the SPARK technology, by democratising the use of proof techniques.
Contributions have been just as effective on an academic level as they have on industry technology transfer results. On the academic side, the LabCom's work has resulted in three publications in international journals and 10 peer-reviewed publications in international conferences.
On the technology transfer side, SPARK was successfully adopted in the space and defence sectors during the duration of the LabCom. A collaboration with Thales led to the joint writing of a public SPARK adoption guide between AdaCore and Thales, used by other teams at Thales and by teams at other companies. These initial successes should be followed by other in the avionics sector and related fields: air traffic, rail and security (with major SPARK clients already for each of them), space and defence. SPARK is also beginning to be used in the medical equipment and autonomous vehicles (cars, drones) sectors.
Finally, two of the three Inria researchers recruited during the duration of the LabCom have been hired by AdaCore.
- Current follow-up actions
The Inria joint laboratory is continuing and a new phase is currently in progress, led by the Toccata team, with AdaCore as a partner but also extending to an additional partner. Why3 software continues to be used by industry or academic actors, as well as in teaching.
When, in 2010, we sought to modernise our formal program analysis tool, we naturally turned to the Toccata team which was already developing the Why3 tool and had demonstrated its scientific advances and technological maturity during successful industry adoption experiences. We have employed two former PhD students from this team and set up a collaborative project with Toccata, then a LabCom, and we are continuing this collaboration today with the proposal for a new Inria joint laboratory. The choice made by the Toccata team to develop freely licenced software and their continued support to the industry users have been decisive factors in the success of this joint venture.
Cyrille Comar, CEO of AdaCore
For the Toccata research team, the collaboration with the SME AdaCore through the ProofInUse joint laboratory is very fruitful. The presence of two Inria engineers working on the project full-time - who spend half of their time on the company's site - enables a very close collaboration, allowing us to be as close as possible to the challenges posed by the industrial applications. The icing on the cake is that this work also results in high-level academic publications.
Claude Marché, head of the Toccata team and leader of the ProofInUse laboratory