Symbolic execution

Symbolic execution is a program analysis technique that explores execution paths using symbolic rather than concrete inputs. Instead of running a program with specific values (e.g., x = 5), symbolic execution treats inputs as mathematical variables and tracks the constraints under which each path is reachable. When a branch depends on a symbolic condition, the execution forks: one path assumes the condition is true, the other assumes it is false. A SMT solver such as Z3 is then used to check whether each path's constraints are satisfiable — determining whether any concrete input can actually drive execution down that path.

The technique bridges fuzzing and formal verification: it has the systematic completeness of formal methods for paths it can explore, and the concrete precision of testing for the paths it reaches. Its central limitation is path explosion: the number of paths grows exponentially with program size, making symbolic execution impractical for large systems without aggressive path pruning or hybridization with concrete execution.

Symbolic execution is the closest we have come to making programs transparent — to reading their behavior as one reads a mathematical proof. That transparency is partial and fragile, but it is real. The programs we cannot analyze symbolically are the programs we do not truly understand.