Technika analizy oprogramowania, w którym wykonanie programu jest symulowane za pomocą symboli, takich jak nazwy zmiennej, zamiast rzeczywistej wartości dla danych wejściowych, a program wyjścia są wyrażane jako wyrażenia logiczne i matematyczne, dotyczące tych symboli.