LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Noticias » Estudiantes de doctorado

BOTBOL Vincent

Doctor
Equipo : APR
Fecha de salida : 25/12/2018
https://www-apr.lip6.fr/~botbol/
Dirección de investigación : Emmanuel CHAILLOUX
Co-supervisión : 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.
Defensa : 13/09/2018 - 14h - Site Jussieu 25-26/105
miembros del jurado :
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

Publicaciones 2013-2018

 Mentions légales
Mapa del sitio |