Une technique d'analyse de logiciels dans lequel l'exécution du programme est simulée à l'aide de symboles, tels que les noms de variables, au lieu des valeurs réelles pour les données d'entrée et sorties de programme sont exprimées sous forme d'expressions logiques ou mathématiques impliquant ces symboles.