L'écriture correcte d'algorithmes concurrents est difficile. Les méthodes les plus répandues de test ne sont guère utiles dans le contexte des programmes concurrents, en raison des comportements non-déterministes de ces programmes, et du fait que certains bugs ne se manifestent que dans un contexte spécifique (par exemple, dans le modèle mémoire simplifié propre à un matériel donné).

La vérification de modèle est une technique formelle qui permet d'identifier les bugs des programmes concurrents en explorant systématiquement les différentes traces d'exécution d'un programme dans un environnement contrôlé.

Dans le cadre de ce projet, nous développons de nouvelles techniques pour résoudre ce problème, en essayant d'améliorer les outils de vérification du modèle existant pour les programmes concurrents, et en les mettant à l'épreuve dans des projets logiciels de production.