Structures de données dynamiques.

L´état de la mémoire d´un programme dynamique peut être représenté par un graphe où les sommets représentent des objets et les arcs modèlisent des pointeurs entre les objets [#!pointeur!#]. Les modifications apportées par un programme, à travers des affectations de pointeurs seront représentées comme un système de réécriture de graphes. En bref, une règle de réécriture de graphes décrit le remplacement d´un arc du graphe initial par un autre graphe. L'ensemble des termes atteignables par de telles règles reste un graphe. Pour représenter des graphes de façon efficace on propose d'utiliser un ensemble de traces avec une relation de congruence (modèle ``storeless'' [#!storeless!#]). Les ensembles de graphes pourraient être représentées par des formules dans la logique monadique de première ordre sur des ensembles de traces.