Multithreading et données dynamiques.

Dans les cas où des structures de données sont partagées entre des différents threads, les problèmes qui se posent sont liées essentiellement aux propriétés de blocage et d'exclusion mutuelle. Afin de pouvoir traiter ces problèmes dans un contexte d´allocation dynamique de mémoire, il faut insérer dans le graphe représentant la mémoire des informations concernant l´identité des threads et les relations entre les threads et les objets. Par exemple, en JAVA les threads se synchronisent utilisant des moniteurs qui appartient à des objets. Le fait que un thread a acquis l´accès à un moniteur peut être représente par un arc spécial. Trouver des blocages dans un programme concurrent est équivalent à trouver des cycles dans le graphe formé par de tels arcs.
 
Pour toute classe de réécriture ainsi défini, le problème principal que nous traitons est celui d´atteignabilité d´un ensemble de termes : étant donné un ensemble de termes et un terme initial, s´il existe un terme dans l´ensemble qui est atteignable, par une séquence finie de transitions, à partir du terme initial. Il s´agit donc de générer une représentation finie de l'ensemble de termes atteignables et de décider si l´intersection avec l´ensemble donné est vide. Pour cela il faut trouver des formalismes pour représenter des ensembles de termes dans quelles l´intersection des ensembles est calculable et décider si une représentation est vide soit possible.

Un exemple concret consiste à modéliser un programme avec des appels à des procédures récursives. Ceci est représenté par un système de réécriture du préfixe. L´ensemble des termes atteignables est un ensemble régulier de mots qui est précisément représenté par un automate fini dont la construction suit une procédure efficace. Le problème d'intersection et de décider si un langage est vide ont ici des solutions classiques.

Dans des cas où il n´est pas possible de trouver des représentations exactes, il est possible se limiter à des approximations qui représentent des surensembles de la fermeture transitive d´un système de réécriture. La perte de précision dans ce cas peut donner des faux contre-exemples. Pour ensuite traiter ce problème, on envisage des techniques de raffinement pour l´abstraction utilisée. L'idée ici est de guider l´abstraction par la propriété à vérifier.