LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Aktuelles » Doktoranten

BOTBOL Vincent

Doktor
Forschungsgruppe : APR
Datum, an dem das LIP6 verlassen wurde : 25.12.2018
https://www-apr.lip6.fr/~botbol/
Forschungsleitung (Direction de recherche) : Emmanuel CHAILLOUX
Co-Betreuung : LE GALL Tristan (CEA)

Static analysis of concurrent programs with numerical variables

Verifying distributed systems is a difficult problem on both theoretical and practice levels, in particular when systems are capable of local numerical computations. The goal of this thesis is to provide a formal verification method of such systems.
We present a general model, based on abstract interpretation, allowin the construction of static analyses for systems of communicating processes. Our methodology is inspired by Regular Model Checking where the set of program states are represented as lattice automata and the program semantics are encoded using rewriting systems applied on the language recognized by the automata. This model offers the possibility of expressing communications between processes as well as dynamic creation/destruction of process. Using the abstract interpretation methodology, we are able to provide a sound over-approximation of the reachability set of programs allowing us to verify numerical safety properties. We implemented this method allowing us to automatically analyse programs that use the distributed computation library MPI/C.
Verteidigung einer Doktorarbeit : 13.09.2018 - 14h - Site Jussieu 25-26/105
Mitglieder der Prüfungskommission :
Ahmed Bouajjani, Université Paris Diderot (Paris 7) [Rapporteur]
Laure Gonnord, Université Claude Bernard (Lyon 1) [Rapporteur]
Antoine Miné, Sorbonne Université (Paris 6)
Gaétan Hains, Huawei Technologies
Emmanuel Chailloux, Sorbonne Université (Paris 6)
Tristan Le Gall, CEA List

Publikationen 2013-2018

 Mentions légales
Plan |