LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » 新闻 » 在读博士

BOTBOL Vincent

毕业博士
科研组 : APR
离开日期 : 2018-12-25
https://www-apr.lip6.fr/~botbol/
责任导师 : Emmanuel CHAILLOUX
助理责任导师 : 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.
答辩 : 2018-9-13 - 14h - Site Jussieu 25-26/105
评委会 :
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

2013-2018 刊物

 Mentions légales
网站导航 |