En informática, 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 informáticos 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. Normalmente, esto se logra aumentando el dominio sobre el cual se lleva a cabo 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 concreto del sistema que se simula indirectamente.
Debido a 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 trayectoria simbólica (STE) y la evaluación de trayectoria simbólica generalizada (GSTE) se basan en esta idea de simulación simbólica.