Symbolic simulation

Typically this process models the complete state of the system at individual points in a discrete linear time frame, computing each state sequentially from its predecessor.

Models for computer programs or VLSI logic designs can be very easily simulated, as they often have an operational semantics which can be used directly for simulation.

This is typically achieved by augmenting the domain over which the simulation takes place.

A symbolic variable can be used in the simulation state representation in order to index multiple executions of the system.

[1] For each possible valuation of these variables, there is a concrete system state that is being indirectly simulated.