Dynamic symbolic execution is a static program analysis technique that can reason about symbolic
inputs. The word “dynamic” refers to the fact that concrete and symbolic values can be mixed
on an execution path [1]}.
Dynamic symbolic execution has two major flavors: concolic and execution-tree generation based.
A symbolic execution engine typically interprets the instructions of an
intermediate language, such as the LLVM IR [2]}, [3]}, so that expressions that involve symbolic
values are manipulated according to the semantics of the instruction.
In this paper, we focus on the execution-tree generation based approach.
When interpreting conditional branch instructions with symbolic branch conditions, a symbolic
execution engine checks the satisfiability of the branch condition for each target using an SMT solver
and to simulate each feasible target it generates a separate path.
On each path it conjoins the symbolic branch conditions to generate the path constraint.
So, the symbolic execution
execution engine generates a tree of symbolic execution paths or states, where the internal nodes with multiple children
denote branching points and each leaf node denotes a completed execution corresponding to an
equivalence class of the input space.
A challenge in symbolic execution is the well-known path explosion problem as the tree of executions
may grow exponentially with the increasing number of branching instructions.
So, symbolic execution is typically configured to run up to some timeout value.
