SUZANNE Thibault

Doktor
Forschungsgruppe : APR
Datum, an dem das LIP6 verlassen wurde : 31.10.2017
https://lip6.fr/Thibault.Suzanne

Forschungsleitung (Direction de recherche) : Antoine MINÉ

Verification by Abstract Interpretation Under Weakly Consistent Memory

Static analysis aims to certify critical software by establishing the absence of errors amongst every possible execution of a given program. Abstract interpretation provides a general theoretical framework to build such analysis that are sound-by-design: they take every possible behaviour of the target into account.
In this thesis, we address the verification of concurrent programs that run in weakly consistent memory models. In addition to sequentially consistent executions that match the interleavings of the threads, these models allow counter-intuitive behaviours that further complicate human reasoning.
We propose dedicated abstract domains to analyse the programs that run under such models. Supported by experimental results, we show how these domains, by means of adapted iteration methods, allow precisely verifying the correction of typical concurrent programming algorithms.
To improve the scaling, we extend this work to the design of a thread-modular analysis. We show by experimentations how, by leveraging specific abstractions and an optimised iteration strategy, this method allows efficiently analysing programs that involve a greater number of threads.
We eventually define abstract domains allowing to precisely infer relations that are specific to the memory model, in order to certify programs entailing complex invariants.

Verteidigung einer Doktorarbeit : 26.02.2019

Mitglieder der Prüfungskommission :

M. David Pichardie (ENS Rennes, Irisa), [Rapporteur]
M. David Monniaux (Verimag, CNRS), [Rapporteur]
M. Antoine Miné (LIP6, Sorbonne Université)
M. Emmanuel Chailloux (LIP6, Sorbonne Université)
M. Luc Maranget (Inria Paris)
M. Xavier Rival (École normale supérieure, Inria)

Datum, an dem das LIP6 verlassen wurde : 31.10.2017

Publikationen 2016-2019

Mentions légales
Plan