Dé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
Comité de programme
workshop on "Practical Aspects of High-Level Parallel Programming" (PAPP 2012)
Groupe de travail LaMHA
La seconde journée du groupe de travail LaMHA du GDR GPL a eut lieu au LIFO le 14 décembre 2010.