Aurèle Barrière, lauréat du EAPLS Best Dissertation Award 2023

/medias/photo/aurele-barriere_1747843071149-jpg

Sa thèse, soutenue le 19/12/2022, portait sur la "Vérification formelle de compilation à la volée", une technique pour exécuter des programmes, où l'exécution est mélangée à des optimisations. Les compilateurs à la volée se distinguent par leur efficacité, mais aussi par leur complexité. Par exemple, ils réutilisent des techniques variées: certains contiennent des interprètes pour exécuter leur programme, mais aussi des compilateurs traditionnels pour générer du code machine optimisé.Ils utilisent également des techniques qui leur sont propres comme la spéculation, qui consiste à prédire le comportement futur du programme et générer du code particulièrement rapide si cette prédiction s'avère vrai. Cette grande complexité peut être à l'origine de bugs. Cette thèse s'attelle à leur vérification formelle, dans le but de développer des compilateurs à la volée dont on peut prouver formellement qu'ils se comportent comme spécifié par la sémantique du programme qu'ils exécutent.

Le jury a considéré que la thèse d’Aurèle était un travail exceptionnel. Selon les conclusions du jury "L’application des méthodes de vérification formelle à la compilation à la volée est particulièrement novatrice et pose de nombreux défis. La contribution d’Aurèle Barrière montre qu’une telle vérification est désormais possible, et ouvre la voie à de nouvelles applications pour des compilateurs à la volée réalistes. La thèse peut déjà être utilisée comme un ouvrage de référence introduisant la compilation à la volée et la vérification formelle de compilateurs à la volée."