Un premier pas vers une méthode d´analyse efficace est de définir le domaine sémantique avec la relation de transition entre deux éléments du domaine (états). A présent, pour chacun des aspects auxquels on s´intéresse dans le cadre de ce projet (multithreading, données et contrôle dynamique) il existe des représentations classiques : la récursion peut être modélisée en utilisant une pile, la paramétrisation peut être modélisée par des tableaux ou des compteurs (souvent il suffit de savoir combien de processus sont dans un état de contrôle) et la structure dynamique de la mémoire peut être représentée par un graphe. Afin d´obtenir des nouvels modèles adéquats à la vérification des programmes qui combinent plusieurs sources de difficulté (multithreading et procédures récursives ou allocation dynamique de mémoire), il ne suffit pas d´effectuer une combinaison directe (produit cartésien) de domaines existantes et de relations de transition. Un des problèmes serait donc d´exploiter les relations entre les modèles en trouvant des dominateurs communs, pour définir des représentations compactes qui permettront que la vérification soit tractable.
Notre approche à la définition de modèles est basée sur des techniques de réécriture. En bref, un système de réécriture est un ensemble fini de règles de transformation d´un terme dans un autre. Un terme peut être soit un mot fini (sur un alphabet donné), un arbre ou un graphe. La puissance expressive d´un système de réécriture dépend du contexte dans lequel les règles peuvent être appliquées. Par exemple, le réécriture du préfixe est équivalente aux automates a pile alors que la réécriture des mots en général est équivalente aux machines de Turing.
Cette puissance expressive permet d´utiliser les systèmes de réécriture comme base commune pour le développement du modèle. Il s'agit concrètement d´identifier des classes de réécriture pour la modélisation de chacun des aspect discuté avant. Dans le cadre de ce projet on va poursuivre les directions de travail suivantes :