Una tecnica di analisi del software in cui l'esecuzione del programma è simulato mediante simboli, ad esempio nomi di variabili, anziché i valori effettivi per i dati di input, e programma uscite sono espressi come espressioni logiche o matematiche che coinvolgono questi simboli.