Hi: It seems that Klee can only work on forward symbolic execution for whole program, starting from the main entry point. I was wondering whether Klee can do backward symbolic execution? Especially, do backward symbolic execution on sub-range of program starting from false assertion point to the fix point, and only cares about the paths on slice in that sub-range. It is some kind of weakest-precondition calculation for the false assertion. Thanks in advance.
-- cheers~!
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
