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.

Publications 2013-2022

• 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”, soutenance de thèse, soutenance 13/09/2018, direction de recherche Chailloux, Emmanuel, co-encadrement : 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)