Partager cette page :

Entretien avec Delphine Demange

Lauréate du prix Gilles Kahn 2013

Actuellement maître de conférences à l'Université de Rennes 1, Delphine Demange est lauréate du prix Gilles Kahn 2013 pour sa thèse sur les "Fondements sémantiques des représentations intermédiaires de programmes" au sein de l'équipe Celtique à l'IRISA / INRIA Rennes. Elle est entrée en tant que magistérienne au département Informatique et télécommunications de l'ENS Rennes, après un L1 et L2 à l'IFSIC.

/medias/photo/ensrennessif_1395839268491.jpg

Pouvez-vous nous présenter votre parcours en quelques mots ? J'ai repris mes études en 2004, en Licence d'Informatique à l'Université de Rennes 1. J'ai intégré en 2006 le Magistère Informatique et Télécommunications (diplôme co-habilité par l'Université de Rennes 1 et l'ENS Cachan -Antenne Bretagne, récemment devenue l'ENS Rennes). J'ai ensuite fait le Master de recherche en Informatique de Rennes 1 en 2008. Après un stage de Master de 5 mois à l'IRISA (équipe Celtique), en vérification de programme, je me suis inscrite en thèse en 2009 dans le même domaine à l'ENS Cachan - Antenne de Bretagne, sous la direction de Thomas Jensen et David Pichardie, dans l'équipe Celtique. Après la thèse, fin 2012 j'ai fait un an de post-doctorat à l'Université de Pennsylvanie (USA), dans le groupe de Benjamin C. Pierce, sur un projet alliant vérification et sécurité. J'ai depuis passé des concours de recrutement, et je suis Maître de Conférences à l'Université de Rennes 1 depuis la rentrée 2013. Y-a-t il une rencontre ou une découverte d'un domaine en particulier qui a été déterminante dans votre choix professionnel ? Comment et pourquoi vous êtes vous orientée vers la rechercher et dans ce domaine ? L'informatique m'intéresse depuis que je suis toute petite. C'est à l'école primaire que j'ai eu ma première expérience de programmation (sur un SMT Goupil!). Il y a toujours eu aussi un ordinateur à la maison, et, je bricolais souvent dessus. C'est en reprenant mes études, après une interruption de 2 ans, que je me suis ré-orientée vers cette discipline. J'hésitais encore à l'époque entre les mathématiques et l'informatique. C'est en discutant avec mes professeurs et encadrants de TP de leurs sujets de recherche respectifs que je me suis décidée. C'est aussi eux qui m'ont parlé du Magistère Informatique et Télécommunications et qui m'ont encouragée à sauter le pas. Le magistère offre une formation approfondie à la recherche en complétant le cursus universitaire traditionnel avec des cours spécifiques et des stages de recherche en France et à l'étranger. C'était donc la voie royale pour la recherche et l'enseignement supérieur. Son slogan "Formation à la recherche, par la recherche" m'a tout de suite convaincue, et les stages de recherche en France et à l'étranger ont été un élément déterminant. Vous avez obtenu le prix Gilles Kahn 3023 pour votre travail réalisé au sein de l'équipe Celtique. Pouvez-vous nous en dire plus ? Mes travaux de thèse portent sur la preuve de compilateurs et vérifieurs statiques de programmes. Le but final est d'assurer, par une preuve mathématique et assistée par ordinateur, que les compilateurs compilent correctement les programmes (i.e. ils n'ajoutent pas de nouveaux comportements aux programmes), et que les vérifieurs calculent des propriétés sur des modèles corrects des programmes (si le modèle du programme ne comporte pas d'erreur, alors le programme d'origine n'en comporte pas non plus). Les vérifieurs statiques et les compilateurs ont pour point commun d'analyser (et de transformer) les programmes qu'on leur fournit en entrée. Pour simplifier leurs analyses, ils travaillent non pas sur des programmes bruts, mais sur des représentations intermédiaires (IR) de ces programmes, qui se prêtent bien au type de calculs (parfois très coûteux) qu'ils ont à effectuer. Mes travaux de thèse étudient d'un point de vue sémantique et formel, ces IRs. En effet, la preuve formelle du code des compilateurs et vérifieurs réalistes ne peut être envisagée sans considérer les IRs comme levier. Si, en pratique, elles sont utilisées pour leurs propriétés sémantiques, elles ne devraient donc pas uniquement simplifier l'implémentation des algorithmes impliqués, mais elles devraient aussi en simplifier la preuve de correction. Nous avons d'abord étudié une IR basée registre pour le bytecode Java, qui est utilisée en première passe de tous les compilateurs et analyseurs bytecode. Nous avons prouvé un théorème de correction sur son algorithme de génération, qui explicite ce que la transformation préserve (l'initialisation des objets, les exceptions) mais aussi ce qu'elle modifie et comment (l'ordre d'allocation des objets). Cette IR fait maintenant partie de Sawja, une libraire OCaml pour le développement d'analyses statiques de Java, qui est développée dans l'équipe Celtique. Nous avons aussi étudié la forme SSA, une IR au coeur des compilateurs et vérifieurs modernes. Nous avons implanté et prouvé en Coq un middle-end SSA pour le compilateur C vérifié CompCert. Pour la preuve des optimisations, nous avons identifié et prouvé un invariant sémantique de SSA clé pour le raisonnement équationnel. Enfin, nous nous sommes intéressés à la sémantique des IRs de Java concurrent. La définition actuelle de cette sémantique, le Java Memory Model (JMM) autorise les optimisations agressives des compilateurs et des architectures parallèles. Extrêmement complexe, elle ne se prête pas bien au raisonnement formel. En ciblant les architectures x86, nous avons proposé un sous-ensemble du Java Memory Model plus intuitif et adapté à la preuve formelle. Nous avons également caractérisé ce modèle axiomatiquement, par les réordonnancements mémoire qu'il autorise, et cette preuve peut se factoriser sur les IRs objet d'un compilateur. Pourquoi avoir choisi cet objet d'étude ? D'où vous vient le goût pour cette matière ? Depuis ma première année de licence, la programmation m'amusait beaucoup, mais j'étais curieuse de comprendre ce qu'était vraiment un programme. Le déclic s'est vraiment produit lorsqu'on m'a présenté les fondements sémantiques des langages de programmation : les programmes devenaient alors des objets d'étude en eux-mêmes. Ensuite, le thème de la vérification vient très naturellement : étant donné un programme et sa spécification (i.e. une propriété sémantique), comment s'assurer qu'il la respecte bien? Ce que j'apprécie particulièrement dans le domaine de la vérification de programmes tient en ce que les modèles sur lesquels nous conduisons nos preuves sont très réalistes, puisqu'il s'agit de leur sémantique. D'autre part, la vérification assistée par ordinateur nous permet de prouver des programmes de plusieurs milliers de lignes de code (une preuve qu'il serait donc impossible de faire à la main, sur papier). Mais cela ne rend pas les preuves gratuites : il est donc capital de concevoir des techniques de preuve qui passent à l'échelle (en termes de taille des programmes, mais aussi de complexité des langages à traiter, et des algorithmes utilisés). Mettre en place de telles techniques est tout à fait passionnant ! Quels sont vos projets à venir ? Je souhaite continuer en recherche académique, et continuer d'étendre le rayon d'action des techniques de vérification, pour du logiciel (et plus généralement des systèmes) toujours plus sûr(s). Les prochains défis auxquels nous nous attaquons concernent la vérification des techniques de compilation optimisantes pour les langages de haut-niveau, en y incluant les aspects les plus difficiles des langages modernes, comme la gestion de la mémoire, la concurrence et les modèles de mémoire faibles. Sur un autre axe, nous nous intéressons également à étendre les compilateurs vérifiés de sorte à ce qu'ils fournissent, en plus, des garanties de sécurité sur les programmes assembleurs générés.

Thématique(s)
Diffusion des savoirs, Recherche - Valorisation

Mise à jour le 17 avril 2014