Dynamic Symbolic Execution Flashcards
symbolic execution
In
this approach, input variables are represented symbolically instead of by concrete
values. The program is executed symbolically, and symbolic path constraints are
collected as the program runs. At each branch point, we invoke a theorem prover to
determine whether a branch can be taken; if so, then we take the branch, otherwise,
we ignore the branch as dead code.
Dynamic Symbolic execution(DSE)
it initially sets the input values of the function to be tested
randomly, and observes the branches of computation that are taken. It also keeps track
of constraints on the program’s state symbolically.
Upon reaching the end of some computational path, DSE will backtrack to some
branch point and decide whether there is a satisfying assignment to the program’s
input variables that allows the other branch to be taken at that point. If so, the solver
generates such an assignment, and DSE continues onward. If not, then DSE ignores
that branch as dead code.