L'objectif du test formel est d'obtenir un sous ensemble de tous les tests possibles qui satisfait un certain critère de couverture. Ce sous-ensemble est communément appelé jeu de test et le critère de couverture est défini à partir de la spécification formelle du système, qu'on peut représenter sous la forme d'un automate. Ma recherche s'articule autour de méthodes d'explorations probabilistes de ces modèles qui garantissent une bonne couverture du critère attendu, quelle que soit la topologie du modèle exploré.

Ayant une formation d'ingénieur à la base, j'ai pris l'habitude de développer des outils (généralement en C++) pour expérimenter mes travaux de recherche. Ainsi, Rukia est une bibliothèque C++, sous licence LGPL, qui permet de tirer, dans des graphes au format GraphViz, des chemins d'une longueur fixée en garantissant une couverture uniforme parmi tous les chemins.

Pendant la préparation de mon doctorat, j'étais moniteur au département informatique de l'IUT d'Orsay. J'y ai donné des cours d'algorithmique et C++ en première année et j'étais responsable d'un projet robotique pour les deuxième année. Ce projet sert à piloter par Internet un robot qui a été construit par l'IUT de Cachan.