English versionDéveloppement de programmes parallèles sûrs
Je m'intéresse actuellement au développement de programmes parallèles sûrs. Ma recherche porte notamment sur l'utilisation d'un assistant de preuve pour prouver la correction fonctionnelle de programmes parallèles et sur l'utilisation de squelettes algorithmique pour factoriser les efforts de développement et de preuve de correction.
Thèse
Dans mes travaux de thèse, ce développement sûr repose sur un plongement superficiel du langage parallèle fonctionnel BSML dans le langage de l'assistant de preuve Coq.
L'utilisation de squelettes algorithmiques permet la construction de programmes parallèles sûrs avec un effort de preuve minimal.
Ma thèse et les développements liés sont disponibles ici
Encadrement
co-encadrement de la thèse de Victor AllombertComité de programme
Workshop International "Practical Aspects of High-Level Parallel Programming" (PAPP 2012, 2016 and 2017)
Symposium International on High Level Parallel Programming and Applications (2015)
Workshop International Interaction and Concurrency Experience (ICE) (2016)
Groupe de travail LaMHA
Je suis responsable du groupe LaMHA du GDR GPL depuis 2015.