Symbolic Execution

Origin. King (1976). Execute with symbolic values instead of concrete. Accumulate path conditions. Explore all paths systematically. Foundation for testing and verification.

Models. Variables hold symbolic expressions. Branches create path conditions. Constraint solving for feasibility. Path explosion main challenge.

Formalism.

Symbolic state: σ = (pc, ρ, π) where:

pc: program counter
ρ: symbolic store (var → symbolic expr)
π: path condition (boolean formula)

Symbolic expressions: e ::= c | x | e + e | e * e | ... Built from constants, symbols, operators.

Assignment: (pc, ρ, π) →[x := e] (pc', ρ[x ↦ ρ(e)], π)

Conditional: (pc, ρ, π) →[if(e)] (pc_t, ρ, π ∧ ρ(e)) if SAT(π ∧ ρ(e)) (pc_f, ρ, π ∧ ¬ρ(e)) if SAT(π ∧ ¬ρ(e)) Fork execution on both branches.

Assertion checking: assert(e): check SAT(π ∧ ¬ρ(e)) If SAT: assertion can fail. Model gives concrete counterexample.

Concolic execution: Concrete + symbolic together. Concrete guides exploration. Symbolic enables path deviation.

Path merging: Combine paths with disjunctive conditions. Reduces exploration, complicates constraints.

Symbols.

Symbol	Unicode	Name	Meaning
σ	U+03C3	Sigma / Symbolic state	The triple (pc, ρ, π)
ρ	U+03C1	Rho / Symbolic store	Maps each variable to a symbolic expression
π	U+03C0	Pi / Path condition	Constraint accumulated along the path taken
pc	—	Program counter	Next instruction of the symbolic state
e	—	Symbolic expression	Term over constants, input symbols, and operators
↦	U+21A6	Rightwards arrow from bar / Store update	ρ[x ↦ ρ(e)], rebinding one variable
→	U+2192	Rightwards arrow / Symbolic step	Transition between symbolic states
∧	U+2227	Logical and	Extends the path condition with a branch guard
¬	U+00AC	Not sign	The negated guard on the false branch
::=	—	Grammar production	Defines the symbolic expression language
SAT	—	Satisfiable	The path is feasible; a model is a concrete input
assert	—	Assertion	Checked by testing SAT(π ∧ ¬ρ(e))

Metatheory. King's 1976 formulation has an exact characterization behind it: the path condition π describes precisely the set of inputs that drive execution down that path, so the paths partition the input space and each path's constraint is neither an over- nor an under-approximation. Two consequences follow. A model of π ∧ ¬ρ(e) at an assertion is a concrete failing input, so reported faults are true positives; and the disjunction of the path conditions of all terminating paths covers the terminating behaviour, so exhaustive exploration would be a decision procedure. Exhaustive exploration is what is unavailable: the number of paths is exponential in the number of branches and unbounded when a loop's trip count depends on input. Feasibility is delegated to a solver, so the method is complete only relative to the theory the program's operations generate — decidable for linear arithmetic and for bit-vectors, undecidable once nonlinear integer arithmetic appears, by Matiyasevich's 1970 solution of Hilbert's tenth problem. Concolic execution (DART, Godefroid, Klarlund, and Sen 2005; CUTE, Sen, Marinov, and Agha 2005) substitutes concrete values wherever symbolic reasoning stalls, restoring progress at the cost of the paths thereby pruned.

Applies to. KLEE, SAGE, Angr. Bug finding. Test generation. Malware analysis. Security testing.

Limitations. Path explosion is structural rather than incidental: n sequential two-way branches give 2ⁿ paths, and a loop whose trip count is an input has no finite set of paths at all, so every terminating search is a partial exploration and the absence of a reported fault carries no information. Feasibility is decided by the solver, so the technique inherits its boundaries exactly — nonlinear integer constraints are undecidable, and a constraint that inverts a cryptographic hash is satisfiable in principle and unreachable in practice. Symbolic reasoning stops at the edge of the modelled code: system calls, libraries, and hardware are either hand-modelled, in which case soundness is relative to that model, or concretized, which silently discards the paths the concrete value forecloses. Path merging trades the number of paths for the size of the constraint, and the disjunctive path conditions it produces are the shape solvers handle worst.