Symbolic execution

Symbolic execution is a static verification technique in which a program is "executed" with symbols (such as X and Y) as inputs instead of actual values. Variables then hold algebraic expressions of the inputs, and at each branch the condition on the inputs is recorded as a path condition. The result for each path is the output expressed as a formula in terms of the inputs, together with the condition under which that path is taken.

How it works

1. Assign symbolic values to all inputs.
2. Execute statements, updating variables with symbolic expressions.
3. At each if or loop, split into two paths and add the condition (or its negation) to the path condition.
4. A path whose condition cannot be satisfied is infeasible and is dropped.
5. For each feasible path, solve the path condition to get concrete test inputs, or check that the output meets the specification.

Example

int f(int x, int y) {
    int z = 2 * y;
    if (z == x)
        if (x > y + 10)
            error();
    return 0;
}

With x = X, y = Y, we get z = 2Y:

Solving path 3 gives Y > 10, for example Y = 11, X = 22. A random test would rarely find these values, but symbolic execution finds them directly.

Uses and limits

• Uses: verifying that each path meets its specification, automatic test case generation, finding unreachable code and error paths. Tools such as KLEE and Java PathFinder use it.
• Limits: the number of paths grows very fast with loops and branches (path explosion); loops with unknown bounds, pointers and complex arithmetic make expressions hard to solve.