Habilitation

I have defended my Habilitation entitled:

on:

in:

The jury was:

Abstract

Many programs are now concurrent, even in the realm of embedded critical software, such as the avionic industry. These programs are notoriously difficult to design and verify. In this work, we present a static analysis method to ensure the safety of such programs. Static analyses run at compile-time and are automatic. They are approximate, to ensure an efficient analysis. They are nevertheless semantic-based and sound: by employing over-approximations, they infer properties that are true of all executions of the analyzed program and thus cannot miss any bug. Our work is grounded in abstract interpretation, a general theory of the approximation of semantics. The method we propose is thread-modular and can be parametrized by a choice of abstract domains to tune the cost versus efficiency trade-off and adapt the analysis to a target application.

The first part of the talk presents a fundamental result: the formalization as abstract interpretation of a constructive version of Jones' rely-guarantee proof method. This opens the way to automatic and thread-modular property inference. We then present the construction, by abstraction of this semantics, of a static analysis for concurrent programs. The analysis is parametric and can reuse the techniques and abstractions developed to analyze sequential programs. We present partitioning techniques over the scheduler state to take into account synchronisation mechanisms (such as locks and priorities). We also discuss the soundness of the analysis with respect to weakly consistent memory models, which are the norm in modern architectures. In the last part of the presentation, we present AstréeA, a prototype implementation of our analysis based on the Astrée static analyzer, and give experimental results analyzing a large embedded critical industrial application.

Manuscript

Manuscript.

The original manuscript is quite compact, to minimize the number of pages (two columns, small margins, 9 points). You might prefer a version with larger fonts (and only one column). These versions have syntax highlighting. In case you want to print the manuscript, you might prefer the black & white compact version or the black & white large-font version.

Slides

Presentation slides.