L'approche est séduisante : on pourrait ainsi utiliser les puissants outils développés par les spécialistes de l'optimisation (MINLP, programmation semi-définie...) afin de résoudre nos problèmes.

Ce n'est toutefois pas si simple. Les problèmes produits par l'analyse de programme ne sont pas forcément semblables à ceux pour lesquels les outils d'optimisation sont conçus. Par ailleurs, en analyse de programme, on attend des réponses sûres ; or, les outils d'optimisation sont en général numériques (calculs en flottants), à l'exception de quelques implémentations de l'algorithme du simplexe en calcul exact sur les rationnels. Lorsque l'on reprend un résultat numérique, on doit s'attendre à ce que sa vérification en calcul exact puisse donner un résultat négatif.

Enfin, l'analyse automatique de programmes contenant des calculs en virgule flottante nécessite la prise en compte des erreurs d'arrondis de ces programmes. L'approche consistant à assimiler les flottants à des réels est incorrecte, au sens qu'elle permet de démontrer des propriétés fausses. Mais comment utiliser des algorithmes numériques pour démontrer des propriétés mettant en jeu les minuscules marges d'erreur du calcul flottant ?