BOTBOL Vincent

Docteur
Équipe : APR
Date de départ : 25/12/2018
https://lip6.fr/Vincent.Botbol

Direction de recherche : Emmanuel CHAILLOUX

Co-encadrement : LE GALL Tristan (CEA)

Analyse statique de programmes parallèles avec variables numériques

La vérification de systèmes distribués est un problème complexe pour de nombreuses raisons tant théoriques que pratiques, en particulier lorsque ces systèmes sont capables d'effectuer localement des calculs numériques. Le but de cette thèse est de proposer une méthode de vérification formelle de tels systèmes.
Nous présentons un modèle général, basé sur l'interprétation abstraite, permettant de construire des analyses statiques pour des systèmes de processus communicants. Notre méthodologie s'inspire du Regular Model Checking en représentant des ensembles d'états de programmes concurrents sous la forme d'automates de treillis et la sémantique de ces programmes comme la réécriture des langages reconnus par ces automates. Ce modèle nous permet notamment d'exprimer des communications entre processus et des créations/destructions dynamiques de processus. L'utilisation de l'interprétation abstraite nous permet d'obtenir une sur-approximation sûre de l'espace d'atteignabilité des programmes nous permettant ainsi de vérifier des propriétés de sûreté numériques. Nous avons implanté cette méthode permettant d'analyser automatiquement des programmes utilisant la bibliothèque logicielle de calculs distribués MPI/C.

Soutenance : 13/09/2018

Membres du jury :

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

Date de départ : 25/12/2018

Publications 2013-2022

Mentions légales
Carte du site