[klee-dev] Question Regarding Path-based Inductive Synthesis for Program Inversion

[陈小玉]

Hello guys. I recently read article *Path-based Inductive Synthesis for
Program Inversion *and found it very insightful. However, I have
encountered some questions regarding one of the principles discussed in the
paper about symbolic execution. I am writing to seek clarification on this
point.

As in Cond&Loop rule: Rule COND non-deterministically executes one of its
branches. Rule LOOP unrolls a loop one time. Is that means in symbolic
execution, for each iteration of the loop, it unrolls the loop into an
“if” statement.
Then, it randomly chooses either to execute the loop body or to jump to the
else branch (exit the loop). Or it just unroll the loop again and again
util it not meet the requirements of  “While” anymore?
-------------- next part --------------
HTML attachment scrubbed and removed