Pour vérifier des propriétés sur des programmes comportant une structure de contrôle et de mémoire dynamique et non-bornée il est nécessaire de soulever deux verrous principaux :
