En ciencias de la computación, una simulación es un cálculo de la ejecución de algún sistema de transición de estado modelado apropiadamente . Normalmente, este proceso modela el estado completo del sistema en puntos individuales en un marco de tiempo lineal discreto, calculando cada estado secuencialmente a partir de su predecesor. Los modelos para programas de computadora o diseños lógicos VLSI se pueden simular muy fácilmente, ya que a menudo tienen una semántica operativa que se puede utilizar directamente para la simulación.
La simulación simbólica es una forma de simulación en la que se consideran simultáneamente muchas ejecuciones posibles de un sistema. Por lo general, esto se logra aumentando el dominio sobre el que tiene lugar la simulación. Se puede utilizar una variable simbólica en la representación del estado de simulación para indexar múltiples ejecuciones del sistema. Para cada posible valoración de estas variables, existe un estado del sistema concreto que se está simulando indirectamente.
Dado que la simulación simbólica puede cubrir muchas ejecuciones del sistema en una sola simulación, puede reducir en gran medida el tamaño de los problemas de verificación. Técnicas como la evaluación de la trayectoria simbólica (STE) y la evaluación de la trayectoria simbólica generalizada (GSTE) se basan en esta idea de simulación simbólica.