Una técnica de análisis de software en el que la ejecución del programa se simula mediante símbolos, tales como nombres de variable, en lugar de valores reales para datos de entrada y salidas del programa se expresan como expresiones lógicas o matemáticas con estos símbolos.