Uma técnica de análise de software no qual a execução do programa é simulada usando símbolos, tais como nomes de variáveis, ao invés de valores reais para entrada de dados e programa saídas são expressos em expressões lógicas ou matemáticas que envolvem estes símbolos.