Décidabilité et complexité.

Les modèles des programmes visés ont un nombre infini de configurations (valeurs des paramètres et des variables, structure de contrôle, structure de la mémoire, etc.) Ceci pose des problèmes aussi bien théoriques (indécidabilité de manière générale du problème de la vérification), que pratiques (taille est complexité des modèles et de leurs ensembles de configurations accessibles).