During his PhD, Maxime Legoupil studied WebAssembly, a bytecode designed to run code efficiently and safely on the internet and elsewhere. The language was designed to facilitate mathematical reasoning about its behaviour, and the work in this thesis introduces the most ambitious effort to study the language formally, in the form a full program logic and formal proofs of specific safety properties. This logic has been extended to reason about new versions of WebAssembly. These new versions have sometimes not been widely tested yet, hence formal results are a precious tool to understand, validate and complete them, as well as encourage their widespread adoption.

The PhD study was completed at the department of Computer Science, Faculty of Natural Sciences, Aarhus University.

This summary was prepared by the PhD student.

Time: Thursday, 20^th of November 2025 at 13:00
Place: Building Ada 5342, room 333 (Bird Room), department of Computer Science, Aarhus University, Åbogade 34, 8200 Aarhus N
Title of PhD thesis: Formal Reasoning about WebAssembly and Extensions
Contact information: Maxime Legoupil, e-mail: maxime@cs.au.dk, tel.: +45 31455546
Members of the assessment committee:
Senior Researcher Andreas Rossberg, Independent, Germany
Professor Sandrine Blazy, Computer Science Department, University of Rennes, France
Professor Anders Møller (chair), Department of Computer Science, Aarhus University, Denmark
Main supervisor: Professor Lars Birkedal, Department of Computer Science, Aarhus University, Denmark
Co-supervisor: Assistant Professor Jean Pichon-Pharabod, Department of Computer Science, Aarhus University, Denmark
Language: The PhD dissertation will be defended in English

The defence is public.
The PhD thesis is available for reading at the Graduate School of Natural Sciences/GSNS, Ny Munkegade 120, building 1521, 8000 Aarhus C