[Version française]


I have defended my Habilitation entitled:

Static analysis by abstract interpretation of concurrent programs

on:

the 28 May 2013 at 14:00

in:

Amphi Galois (a.k.a Amphi Rataud)
Library Building (NIR), PB floor
École Normale Supérieure
45, rue d'Ulm
75005 Paris
France

The jury was:

Ahmed Bouajjani Université Paris 7 Diderot, France
Patrick Cousot École normale supérieure, France & New York University, U.S.A.
Roberto Giacobazzi Università di Verona, Italy (reviewer)
Éric Goubault Commissariat à l'énergie atomique, France
Nicolas Halbwachs Vérimag, France (reviewer)
Manuel Hermenegildo IMDEA Software Institute & Technical University of Madrid, Spain (reviewer)
Marc Pouzet École normale supérieure, France

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. [English]

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. [English]


Antoine Miné