Stage Master : |
On recrute un stagiaire de niveau Master pour travailler sous la direction de Roberto Amadio et Yann Régis-Gianas sur le projet européen "EU-FP7 Certified Complexity" (CerCo) au sein du laboratoire PPS, situé à Paris.
L’objectif principal du projet CerCo est de vérifier formellement dans un système de preuve type Calcul des Constructions un compilateur du langage C vers un langage assembleur pour micro-contrôleurs, similaire à ceux utilisés dans les systèmes embarqués. En plus de la correction fonctionnelle du compilateur, le projet vise à établir une relation précise entre la complexité concrète du programme source et du programme objet, en particulier en présence d’optimisations. Ainsi le compilateur produira en plus du code objet, des annotations sur le programme source (en langage C) dont la correction sera garantie par une preuve formelle. Les annotations sur le programme source seront utilisées dans des systèmes de preuve semi-automatiques afin de synthétiser des bornes sur les ressources nécessaires à l’exécution du programme C. Enfin, ces méthodes de synthèse seront testés sur les programmes C générés par les compilateurs de langages synchrones comme Lustre et Esterel. Le compilateur et les preuves seront distribués sous des licences libres. Ce travail sera mené en stricte collaboration avec les Universités de Bologne (Andrea Asperti et Claudio Sacerdoti-Coen) et d’Edimbourg (Randy Pollack).
Le stage se focalisera sur le développement et la certification d’un prototype de compilateur (optimisant) annotant les programmes sources (exprimés dans un C simplifié) par des assertions de coût.
De bonnes connaissances en programmation fonctionnelle (OCAML) et en compilation (structure de GCC) sont attendues. Les candidats intéressés peuvent contacter Roberto Amadio ou Yann Régis-Gianas.
Ce document a été traduit de LATEX par HEVEA