Verification de protocoles de sécurité: preuve formelle des algos et amélioration des outils (Verification of security protocols: machine-checked proof of the algos and improvement of the tools)   Preuve formelle d'algorithmes parallèles pour la génération de l'espace d'état et la vérification de protocoles de sécurité. Traduction et extension d'un langage de description des protocoles de sécurité vers une algèbre de réseaux de Petri. Algorithmes parallèles et programmation parallèle fonctionnelle (Parallel algorithms and functionnal parallel programming)   Opérations Matricielles Parallèles en BSML et ses Applications. Une bibliothèque applicative (parallèle) d'algorithmes BSP sur les graphes; implantation générique et expérimentations. Programmation parallèle certifiée (Parallel certified programming)   Certification en Coq d'une implantation distribuée de squelettes de flots. Optimisations certifiées de programmes BSP.