Symbolic execution runs a program using symbolic inputs instead of concrete values and records the conditions required to follow each control-flow path.

For

if x > 0:
    y = x + 1
else:
    y = 0

start with symbolic input $X$. The true branch produces symbolic state

$$y=X+1$$

with path condition

$$X>0.$$

The false branch produces $y=0$ under $X\le0$.

When the analyzer reaches an assertion, it can ask a solver whether the path condition together with the negation of the assertion is satisfiable. A satisfying assignment becomes a concrete counterexample input.

Symbolic execution is path sensitive: it distinguishes different branch histories instead of immediately joining them. This can produce precise bug reports, but the number of paths can grow exponentially with branches and loops, creating path explosion.

Practical systems bound loops, merge states, prioritize paths or combine symbolic reasoning with concrete execution.

Symbolic execution complements abstract interpretation. Abstract interpretation usually merges many executions into a sound approximation; symbolic execution often preserves individual path constraints to reason precisely about particular feasible behaviors.