Xavier Rival: automatically verifying the safety of critical software.

An error in software can have catastrophic human or economic consequences, especially if it is critical software like the kind that controls aeronautical, aerospace, nuclear, medical or automotive systems. How can we be sure that the software will always run without errors? Xavier Rival aims to answer this complex question. The researcher, still in his early thirties and a former École Normale Supérieure student, certainly has his work cut out given that 99% of industrialists verify their software by simply testing all or part of it during runtime, hundreds of times in a row... And banking on the fact that the result will be reproducible.

In the Abstraction team, we are developing methods for automatic code analysis that will allow all the executions of a program to be verified in a single calculation.

In other words, these analysers calculate evidence in the mathematical sense. In addition to the economic benefit (industrial-scale software can be tested in a single day’s calculation), the result is perfectly reliable. It was after the explosion of Ariane 5 in 1996, due to a software error, that software verification tools began to conquer the industrial world. In this context, design work on the Astrée analyser has been ongoing since 2001. Xavier Rival participated in its development during his PhD (École polytechnique) in a laboratory at the École Normale Supérieure. Generally speaking, significant progress has been made in recent years but more particularly on software performing numerical calculations such as those verified by Astrée.

There is still a lot to do for software that handles complex data structures in memory (lists, trees, queues).

"On the other hand, we don't know how to analyse the many embedded software programs quite as efficiently, which are less critical but need to use complex data in memory, such as communication and navigation software, data exchange protocols, etc. That's what my ERC project is about," he explains. It would broaden the scope of application of these tools. Xavier Rival has come up against these complex issues on several occasions, beginning in 2006 as part of a collaboration with Bor-Yuh Evan Chang during his postdoc at Berkeley, and then again when he joined the institute in 2007. Efficient algorithms already existed to automate the analysis of software executing numerical calculations, by decomposing logical properties into simple elements, but there is still a lot to do for software handling complex data structures in memory, whether in the form of lists, trees or queues etc. This makes reasoning and its automation very complex. “Having mulled over my idea for a year or two, I feel ready to face the challenge”, he concludes. His ERC grant will allow him to work with three PhD students, three postdocs and an engineer for five years, as well as to invite professors for short-term collaborations.