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.

En plus de mon statut de doctorant, je suis moniteur au département informatique de l'IUT d'Orsay. J'y donne des cours d'algorithmique et C++ en première année et je suis 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.