[klee-dev] Backward Symbolic Execution

[Cacho]

Hi Saksham, can you paste the links please?.

Thanks

On 06/09/2015 12:48 AM, Saksham Jain wrote:
> 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev