Recherche

Je suis actuellement Doctorant au LaBRI au sein de l'équipe méthodes formelles (MF), dans le groupe modélisation et vérification (MV). Je suis pour cette thèse encadré par Marc Zeitoun et par Frédéric Herbreteau.

Mon sujet de thèse d'origine est "Heuristiques pour représentations symboliques d'ensembles de configurations". J'ai travaillé sur les liens entre logique de Presburger, et automates alternants.

Actuellement, je travaille sur les suites à donner à mon mémoire de Master 2 recherche. Le titre de ce mémoire était "Séparation d'espaces d'états représentés par des langages - Application au calcul d'interpolant sur les ROBDD". Et nous regardons comment utiliser ce calcul d'interpolant dans le cadre du raffinement des états abstraits d'un système dans une approche CEGAR du model-checking.