En informática, una simulación es un cálculo de la ejecución de un sistema de transición de estado modelado adecuadamente . 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. Esto se logra generalmente ampliando el dominio sobre el que 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. [1] Para cada posible valoración de estas variables, existe un estado concreto del sistema que se está simulando indirectamente.
Dado que la simulación simbólica puede abarcar muchas ejecuciones de sistemas en una única 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.