Thèse Compilation Formellement Vérifiée d'Un Langage de Programmation Orienté Interaction H/F - 74

Établissement : Ecole Nationale de l'Aviation Civile
École doctorale : SYSTEMES
Laboratoire de recherche : ENAC-LAB - Laboratoire de Recherche ENAC
Direction de la thèse : Stéphane CONVERSY ORCID 0000000251456476
Début de la thèse : 2026-10-01
Date limite de candidature : 2026-06-30T23:59:59

Avec la démocratisation des appareils interactifs, les utilisateurs s'attendent désormais à interagir avec leurs systèmes par le biais d'interactions tactiles et avancées. Pour faciliter la mise en oeuvre de ces systèmes, des langages de programmation dédiés « orientés interaction » ont été proposés. Ces langages permettent de décrire efficacement à la fois l'apparence du système et son comportement interactif. Ils sont de plus en plus populaires, y compris pour le développement de systèmes critiques. Cependant, peu d'efforts ont été consacrés à la formalisation de ces langages, de leur sémantique ou de leur modèle d'exécution.

L'objectif de ce projet de recherche est de formaliser Smala, un langage orienté interaction développé à l'ENAC.
Smala est un langage réactif, dans lequel le programmeur spécifie la façon dont les événements extérieurs sont propagés et dont le programme réagit, en mettant à jour son état interne et en déclenchant des comportements observables. Ce programme déclaratif de haut niveau peut ensuite être compilé en code impératif qui implémente ces réactions.

Au cours de ce projet, le candidat formalisera le langage et sa sémantique, et implémentera sa compilation vers le langage de bas niveau C. Une partie importante du travail sera consacrée à la vérification de bout en bout du schéma de compilation : le candidat développera une preuve mécanisée que le programme C généré implémente bien le comportement spécifié par le programme source Smala.

Pour ce faire, le candidat utilisera principalement l'assistant de preuves interactif Rocq. En effet, celui-ci comprend des fonctionnalités pour la spécification (de la sémantique de Smala), l'écriture de programmes (le schéma de compilation en tant que programme purement fonctionnel) et les preuves vérifiées automatiquement (relant cette sémantique, la fonction de compilation et la sémantique du C telle que spécifiée dans le projet CompCert).

This project will integrate with the work of the LII team at Ecole Nationale de l'Aviation Civile
(ENAC). Since 2010, the team has been developping Djnn1/Smala2 [6], respectively a framework
and programming language for implementing interactive programs, such as Graphical User Inter-
faces (GUIs). This framework has been used for rapid prototyping for the purpose of Human
Machine Interface (HMI) research, but also to implement critical GUIs, such as the cockpit display
of an electrical helicopter [1], or radar images for air traffic control (see fig. 1). The reference
implementation of Smala is a compiler that generates C++ code using the Djnn framework [6],
where each Smala component is implemented by a corresponding Djnn object. The design of this
implementation does not facilitate formal verification: for instance, there is no guarantee that the
generated program executes in finite time, does not raise an error during execution, or that it
respects the source specification.
In more recent work [7], we have started implementing a more formal toolchain for the language,
based on ideas from synchronous languages [2]. We have formalized a denotational semantic model
for a subset of the Smala language, that we argue is expressive enough to encode all higher-level
constructs from the full language. These semantics specify the behavior of the program as a
synchronous reaction to a given event, which may trigger new events and update the state of the
program. This model was formalized in the Rocq prover 3 [9]. We also implemented an unverified prototype compiler for this subset, which targets Obc, an imperative language formalized in the
Vélus project [4]. Vélus also provides a formally verified compilation pass from Obc to Clight, the
input language of the CompCert [5] verified compiler.