Supervision : Emmanuel CHAILLOUX
Co-supervision : 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.

Phd defence : 09/13/2018

Jury members :

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-2022 Publications

• 2022
  • G. Bau, A. Miné, V. Botbol, M. Bouaziz : “Abstract interpretation of Michelson smart-contracts”, SOAP '22: 11^th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, San Diego, CA, United States, pp. 36-43, (ACM) (2022)
• 2018
  • V. Botbol : “Analyse statique de programmes parallèles avec variables numériques”, thesis, phd defence 09/13/2018, supervision Chailloux, Emmanuel, co-supervision : Le, GALL Tristan (CEA) (2018)
• 2017
  • V. Botbol, E. Chailloux, T. Le Gall : “Static Analysis of Communicating Processes Using Symbolic Transducers”, International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2017, vol. 10145, Lecture Notes in Computer Science, Paris, France, (Springer International Publishing) (2017)
• 2013
  • B. Canou, E. Chailloux, V. Botbol : “Static Typing and JavaScript Libraries: Towards a More Considerate Relationship”, International World Wide Web Conference, dev track, Rio de Janeiro, Brazil, pp. 15-17 (2013)