Compilation Formellement Vérifiée d'un Langage de Programmation Orienté Interaction

Ecole Nationale de l'Aviation Civile; France; Sur place; EUR 40 000 - 60 000; Plein temps

Résumé du poste

Un institut de recherche en aéronautique recherche un candidat pour formaliser le langage Smala et sa sémantique dans le cadre d'un projet de recherche. Le candidat sera chargé de développer la compilation vers le langage C et de vérifier la cohérence du processus. Un master en informatique et une expérience avec les méthodes formelles, le prouveur Rocq, et la programmation OCaml sont exigés. Une connaissance des systèmes de gestion du trafic aérien est un plus.

Qualifications

• Le candidat doit être titulaire d'un master (ou équivalent) en informatique.
• Familiarité avec les méthodes formelles, le prouveur Rocq, OCaml, et la compilation requise.
• Connaissance de la programmation IHM et/ou des systèmes de gestion du trafic aérien appréciée.

Responsabilités

• Formaliser le langage Smala et sa sémantique.
• Implémenter la compilation vers le langage de bas niveau C.
• Développer une preuve mécanisée de la compilation.

Connaissances

Méthodes formelles

Proveur Rocq

Programmation OCaml

Compilation

Formation

Master en informatique ou équivalent

Description du poste

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 œuvre 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).

With the democratization of interactive devices, users now expect to interact with their systems through tactile and advanced interactions. To facilitate the implementation of these systems, dedicated “interaction-oriented” programming languages have been proposed. These languages can efficiently describe both the appearance of the system and the interactive behavior. They are becoming more popular, including for the development of critical systems. However, there has not yet been a lot of effort in formalizing these languages, their semantics or their execution model.

The goal of this research project is to formalize Smala, an interaction‑oriented language developed at ENAC. Smala is, at its core, a reactive language, where bindings written by the programmer specify how outside events are propagated, and how the program reacts by updating its internal state and triggering observable behaviors. This high‑level, declarative program can then be compiled into imperative code that implements these reactions.

During this project, the candidate will formalize the language and its semantics, and implement its compilation into the low‑level language C. A significant amount of work will be dedicated to the end‑to‑end verification of the compilation scheme: the candidate will develop a mechanized proof that the generated C program does implement the behavior specified by the source Smala program. To do so, the candidate will use the Rocq prover as a primary tool. Indeed, it includes facilities for specification (of Smala's semantics), writing programs (the compilation scheme as a purely functional program), and automatically‑checked proofs (relating these semantics, the compilation function, and the semantics of C as specified in the CompCert project).

Début de la thèse : 01/10/2026

Funding category: Concours de l'École Doctorale

Requirements

Le candidat doit être titulaire d'un master (ou équivalent) en informatique. Le candidat doit être familiarisé avec :

• les méthodes formelles
• le prouveur Rocq
• la programmation OCaml
• la compilation

De plus, une connaissance de la programmation IHM et/ou des systèmes de gestion du trafic aérien sera appréciée.

The candidate should hold a master's degree (or equivalent) in computer science. The candidate should be familiar with :

• formal methods
• the Rocq prover
• OCaml programming
• compilation

In addition, knowledge of HMI programming and/or air traffic management systems will be appreciated.