Thèse Interprétation Abstraite pour Webassembly H/F - 40

Établissement : Université Côte d'Azur
École doctorale : STIC - Sciences et Technologies de l'Information et de la Communication
Laboratoire de recherche : Secure Programming Languages & Tools for Security
Direction de la thèse : Manuel SERRANO ORCID 0000000252401610
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-09-30T23:59:59

Cette thèse vise à établir un cadre d'analyse statique correct pour
WebAssembly, un langage cible de compilation largement utilisé,
fondé sur l'interprétation abstraite. L'objectif est de concevoir
des analyses adaptées aux extensions récentes, notamment le
ramasse-miettes, en ciblant des propriétés telles que la nullité et
les types des références afin d'éliminer les vérifications
dynamiques redondantes. D'autres extensions seront également
explorées comme l'interface JIT ou les coroutines. Par ailleurs, les
interactions inter-langages entre Wasm et son environnement hôte
JavaScript feront l'objet d'une étude approfondie. Ces travaux
aboutiront à la conception d'un prototype d'analyseur qui sera
intégré à des compilateurs comme Bigloo ou WasmOCaml et évalué sur
des exemples concrets.

Thèse co-encadrée par M. Manuel Serrano (Inria Splits),
spécialiste de programmation fonctionnelle et compilation et
M. Xavier Rival, spécialiste d'interprétation abstraite et
analyse static (Inria Antique et ENS).

Analyse statique multi-langages WebAssembly + JavaScript.

Interprétation abstraite
Compilation