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
ρ	U+03C1	Rho	Symbolic store
π	U+03C0	Pi	Path condition
SAT	—	Satisfiable	Constraint check

Metatheory. Sound for paths explored. Path explosion: exponential paths. Loops require bounds or summaries. Heap modeling complex.

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

Limitations. Path explosion. Complex constraints (floats, crypto). Environment modeling. Loops and recursion. Scalability.