Eine Software-Analyse-Technik, bei der Programmausführung wird simuliert mithilfe von Symbolen, z. B. Variablennamen, anstatt die tatsächlichen Werte für Eingabedaten und Programm gibt, werden als logische oder mathematische Ausdrücke mit dieser Symbole ausgedrückt.