责任导师 : 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.

2013-2022 刊物