Recherche

Mes travaux de recherche s'inscrivent dans le cadre général de la vérification formelle de programmes par analyse statique. Un des objectifs de l'équipe Celtique de l'IRISA/INRIA Rennes est de développer des méthodes et des outils de vérification.

J'utilise comme modèles formels des programmes les systèmes de réécriture de termes et les automates d'arbres. Ma thèse porte principalement sur l'adaptation de la complétion d'automate d'arbre à la stratégie d'évaluation en profondeur en vue de l'analyse de programmes fonctionnels, notamment ceux rédigés en OCaml.

Thèse

  • Analyse d'atteignabilité pour les programmes fonctionnels avec stratégie d'évaluation en profondeur, soutenue le 7 décembre 2015 à Rennes devant le jury composé de
    • Géraud Sénizergues, Professeur à l’Université de Bordeaux, Rapporteur
    • Pierre Réty, Maitre de conférences à l’Université d’Orléans, Rapporteur
    • Thomas Jensen, Directeur de recherches à l’I.N.R.I.A., Examinateur
    • Hélène Kirchner, Directrice de recherches à l’I.N.R.I.A., Examinatrice
    • Sylvain Salvati, Chargé de recherches à l’I.N.R.I.A., Examinateur
    • Thomas Genet, Maitre de conférences à l’Université de Rennes 1, Directeur de thèse

Articles

Rapports

Logiciel

Je travaille à une version du logiciel Timbuk améliorée pour l'utilisation de la stratégie d'évaluation en profondeur. Une version alpha de TimbukSTRAT est disponible ici.

Présentations

  • Présentation aux journées du GDR GPL, au CNAM, Paris, juin 2014
  • Atteignabilité pour les systèmes de réécriture avec stratégies aux Journées communes LTP - LAC - LAMHA 2012 des GdR GPL et IM, octobre 2012, Orléans
  • Proving Reachability Properties on Term Rewriting Systems with Strategies à IWS 2012, juillet 2012, Manchester

Séjours

  • Séjour dans l'équipe de Luke Ong, à l'Université d'Oxford, janvier–février 2014