FIEEC Carnot Prize for Applied Research: Claude Marché “proves himself”!

Claude Marché: I feel honoured by this prize which recognises the applied-research partnerships we’re running with an industry player who is making a real economic impact. Since 2010, we've undertaken a number of research projects with AdaCore on deductive program verification. This prize has been awarded to me personally, but in my view the Toccata team and AdaCore also deserve to be rewarded.

Yannick Moy: Before joining AdaCore I was part of the Inria ProVal team where Claude worked as my research director, between 2006 and 2009. When I joined this publisher, I proposed replacing the “proof” part of the solution used at that time by the Why3 (formerly Why) opensource technology developed by Inria. That was followed by an industrial partnership leading to multiple collaborations on cooperative projects backed by competitiveness clusters, then by the creation of a joint laboratory (ProofInUse) funded by the National Research Agency (ANR) between 2014 and 2017. We then signed a bilateral cooperation agreement, which runs until 2022, whereby AdaCore funds part of Toccata's research work.

What is computer proofing?

Claude Marché: A number of Inria teams have historically been interested in this topic. Where we at Toccata are breaking new ground is in our decision to use proofing techniques to validate computer programs. In practical terms, mathematical proofs of software demonstrate that the software actually does what it is designed to do and that it meets all the operating dependability criteria defined by the company. Until now, the most common method was to do testing: this technique is effective, but necessarily limited in scope and it is costly. But by using computer proofing, you can test the program in the maximum possible configurations. We have therefore developed a system that allows us to express mathematically all the possible configurations for a program and verify that it always runs in accordance with the user's expectations.

Yannick Moy: We've integrated a number of applications developed by the Toccata project team in our SPARK software-verification environment. As an opensource developer, program-proofing helps us to offer guarantees to users of the software that we design: these companies – for example, Airbus, Altran and Nvidia – pay us for platform support and for our ability to help them use our software in an super-secure way. 

Who uses this type of technology?

Claude Marché: Many companies in the aeronautics and transportation sectors have been interested in it for a long time – they use software for which dependability, effectiveness and security are critical. They spend lots of money testing software and some of them want to optimise their investments by using proofing technology. Our partnership with AdaCore allows us to develop applications for these sectors, and to do it in such a way that our research, which is necessarily highly theoretical, brings practical industrial benefits.

Yannick Moy: This is cutting-edge technology which is attracting more and more interest outside avionics and the railway sector, such as driverless vehicle manufacturers, security specialists, medical devices companies, and providers of cloud computing services. The players in these sectors also have critical dependability requirements to prevent any error or deliberate attack from endangering the lives of their users. This involves, for example, ensuring the absence of security flaws in onboard platforms in vehicles or implanted in patients, while allowing them to be connected to networks like the Internet. It is up to us to understand their needs and to share them with Inria so we can move forward together on the most complex aspects.

What are your goals for the future?

Claude Marché: I want to diversity our ecosystem of partners, for example by working with other publishers of critical programming tools and software intended for other industry sectors. From an academic point of view, my dream is to see our program-proofing tools increasingly being used throughout the design cycle: software proofing at the same time as software development, to ensure that dependability is established much earlier in the process.

Yannick Moy: As for AdaCore, our main task will be to develop technological bricks to facilitate proofing techniques.