[klee-dev] Backward Symbolic Execution

[Saksham Jain]

Hi,

I saw that KLEE doesn't work well in case of loops.E.g.:

int a;
klee_make_symbolic(&a, sizeof(a), "a");
for(int i=0;i<a;i++)
{
   if(i==10000)
      assert(0);
}

For this, KLEE makes 10,000 test cases before it reach assert(0)
instruction.

So I made a program which works in backward fashion i.e. it will start from
assert(0) instruction (i.e. the instruction that I need to find feasibility
of), and try to reach the top(start of main function) (Initially it assumes
every variable as symbolic).
This approach works much faster than forward execution (i.e. KLEE approach).
I found later that this technique is not new and has already been thought
of before.

My question is:* Why is this Backward symbolic execution not popular?*
Because I think it can cover the coverage holes that KLEE isn't able to
achieve.
Is it because in larger programs this alternate approach will be quite
slower?

Can someone also point to me some tool which performs backward symbolic
execution?

Regards,
Saksham Jain
-------------- next part --------------
HTML attachment scrubbed and removed