Symbolic executors work by running the program, computing over both concrete values and expressions that include symbolic variables, which are unknowns that range over various sets of values, e.g., integers, strings, etc.. When a symbolic executor encounters a conditional whose guard depends on a symbolic variable, it invokes a theorem prover (e.g., an SMT solver such as Z3, Yices, or STP) to determine which branches are feasible.
If both are, the symbolic execution conceptually forks, exploring both branches.
Symbolic execution is an attractive approach to solving line reachability, because it is
complete, meaning any path it nds is realizable, and the symbolic executor can even construct a concrete test case that takes that path (using the SMT solver). However, symbolic executors cannot explore all program paths,
and hence must make heuristic choices about which paths to take.
from the linked paper [http://drum.lib.umd.edu//handle/1903/11374]:
Symbolic executors work by running the program, computing over both concrete values and expressions that include symbolic variables, which are unknowns that range over various sets of values, e.g., integers, strings, etc.. When a symbolic executor encounters a conditional whose guard depends on a symbolic variable, it invokes a theorem prover (e.g., an SMT solver such as Z3, Yices, or STP) to determine which branches are feasible. If both are, the symbolic execution conceptually forks, exploring both branches.
Symbolic execution is an attractive approach to solving line reachability, because it is complete, meaning any path it nds is realizable, and the symbolic executor can even construct a concrete test case that takes that path (using the SMT solver). However, symbolic executors cannot explore all program paths, and hence must make heuristic choices about which paths to take.