certes.

cela dit l'interprétation abstraite ça ne fait pas que ça, on peut aussi prouver des propriétes de bon comportement autres. par exemple les drivers de windows vista, pour être spécifiés, doivent être analysés avec un outil d'interprétation abstraite qui prouve tout un tas de trucs bien sur le driver (genre que quand il release un lock il en avait bien acquéri un auparavant, qu'il n'y a pas de deadlocks, qu'on ne corromp pas la mémoire du noyau, etc ...)