Most program analysis runs code with real values: you pass in the number 5, the string “admin”, a JSON body, and you watch what happens. Symbolic execution does something different. Instead of a concrete value, it feeds the program a symbol that stands for any possible input, then works out, branch by branch, exactly which inputs would drive execution down each path. That lets it answer a precise question: what input reaches this specific line?
What symbolic execution actually does
Pick a small function. It takes an amount and a balance and decides whether a withdrawal is allowed.
def withdraw(amount, balance):
if amount > balance:
return "denied"
return balance - amountA normal run needs numbers. You call withdraw(30, 20) and get “denied”. Symbolic execution skips the numbers. It treats amount as a symbol, call it A, and balance as a symbol B. Then it walks the code. When it hits the if, it cannot pick a side, because it does not know the values. So it forks. It follows both branches and remembers, for each one, the condition that had to be true to get there. That remembered condition is the path constraint.
- Path one takes the
if. Its path constraint isA > B. Any input where the amount is larger than the balance lands here and returns “denied”. - Path two falls through. Its path constraint is
A <= B. Any input where the amount is at most the balance lands here and returns the new balance.
Now the useful step. A constraint solver takes a path constraint and hands back concrete values that satisfy it, or tells you none exist. Ask it to satisfy A > B and it might return A = 1, B = 0. Ask it to satisfy A <= B and it might return A = 0, B = 0. You now have a real test input for each path, derived from the code itself rather than guessed.
Why symbolic execution matters for finding bugs
The point is not to enumerate paths for their own sake. The point is to prove that a dangerous line is reachable with a specific input. Take a function with a clear flaw.
def write_slot(n, table):
# table has exactly 8 slots
if n > 100:
table[n] = 1 # n is far past the end of table
return tableThe write on line four is out of bounds whenever the branch is taken. Symbolic execution treats n as a symbol, reaches the if, and records the path constraint n > 100 for the branch that performs the write. Hand that to the solver and it returns something like n = 101. That is not a maybe. It is a concrete input that drives the program to the bad line, which you can drop straight into a test and watch fail.
A path constraint plus a solver turns “this line looks reachable” into “here is the exact input that reaches it.”
This is the difference between a warning and a proof. A cheaper analysis might flag that line as suspicious. Symbolic execution can produce the input that triggers it, which is the evidence a developer needs to believe the finding and fix it.
The honest limit: path explosion
There is a hard ceiling, and it is worth being blunt about it. Every branch forks the analysis into more paths. Two if statements in a row give four paths. Ten give more than a thousand. A loop that can run an unknown number of times multiplies paths on every iteration. This is path explosion, and it is the reason pure symbolic execution does not scale to a whole large program on its own.
Picture a request handler with twenty branches feeding into a parser with its own loops. The number of distinct paths is astronomical, and the solver has to reason about the constraints along each one. You run out of time or memory long before you finish. Anyone who tells you symbolic execution just scans your entire codebase and prints every bug is skipping this part.
How it fits with cheaper analysis
The way to use symbolic execution well is to point it at a small target, not the whole program. You let a lighter analysis do the wide search, then spend the expensive symbolic work only where it pays off. A common shape looks like this:
- Run a fast, whole program pass to find a candidate location, for example a memory write or a query built from user input that might be reachable from an entry point.
- Use reachability analysis to check whether any path even connects the input to that location. If nothing reaches it, you stop and spend nothing more.
- Only for the candidates that survive, run symbolic execution on that slice to produce the actual input that reaches the line, or to prove that the path constraint is unsatisfiable and the warning was a false alarm.
That last case matters as much as the first. When the solver reports that a path constraint has no solution, it has proven the path is infeasible. That is a clean way to rule out a candidate rather than leave it as noise a person has to triage by hand.
A structural model of the code makes the handoff cleaner. When your candidates come out of a code property graph, each one already carries the path from input to sink, so the symbolic step knows exactly which slice to solve instead of the whole function.
Concolic execution in one line
There is a middle option worth knowing by name. Concolic execution mixes concrete and symbolic: it runs the program with a real input to pick one concrete path, keeps the symbolic constraints for the branches along that path, then flips one constraint and asks the solver for an input that takes the other side, which steers exploration toward new paths without forking on every branch at once.
The takeaway
Symbolic execution is a precise tool with a narrow reach. It replaces guessed inputs with symbols, records a path constraint at every branch, and uses a solver to turn a constraint into the exact input that reaches a line, or to prove no such input exists. It cannot swallow a whole large program because paths explode, so it works best as the proving step after a cheaper analysis has narrowed the search. For more on where broad scanning ends and focused reasoning begins, read scanners vs research. Proving that a real input reaches a real flaw, rather than listing patterns that might matter, is exactly the kind of verification UnboundCompute is built around, and you can read how we think about it on our about page.
Frequently asked questions
What is symbolic execution in simple terms?
Instead of running a program with real values, symbolic execution feeds it a symbol that stands for any possible input. At each branch it forks and records the condition that had to be true to take that path, called a path constraint. A constraint solver then turns a path constraint into a concrete input, for example the exact value that reaches a vulnerable line.
What is a path constraint?
A path constraint is the set of conditions that must all hold for execution to follow one particular path. For a function with if amount > balance, the branch that is taken has the path constraint amount > balance and the branch that falls through has amount <= balance. A solver reads a path constraint and returns concrete inputs that satisfy it, or reports that none exist.
What is path explosion and why does it limit symbolic execution?
Every branch forks the analysis into more paths, so two ifs give four paths, ten give over a thousand, and a loop multiplies paths on each iteration. This is path explosion, and it is why pure symbolic execution does not scale to a whole large program on its own. The fix is to point it at a small slice that a cheaper analysis has already flagged, not the entire codebase.
How is concolic execution different from symbolic execution?
Concolic execution mixes concrete and symbolic. It runs the program with a real input to pick one concrete path, keeps the symbolic constraints for the branches along that path, then flips one constraint and asks the solver for an input that takes the other side. This steers exploration toward new paths without forking on every branch at once.
Put an autonomous researcher on your own systems
UnboundCompute is an autonomous security researcher that reasons about how an application fits together and proves the access control and injection bugs it finds. We are opening a small number of founding design partner seats: private early access pointed at a staging target you choose, and a say in what it looks for. If your team ships software worth pressure testing, apply to the design partner program.