[klee-dev] Example of recursive define in real system/ programs

[Loi Luu]

Hi,

I'm working on recursive constraints on KLEE and having some idea now. How
the solver works is like that, for example given a sequence which is
recursively defined as a(n) = a(n-1)*2 + 2. then the solver will find the
exactly formula representing the a(n) based on n. You can look at this
example<http://www.wolframalpha.com/input/?i=RSolve%5B%7Ba%5Bn%5D+%3D%3D+a%5Bn-1%5D%2B%28n%29%21%2C+a%5B0%5D+%3D%3D+1%7D%2C+a%5Bn%5D%2C+n%5D+>
in
wolfram alpha for more understanding

In programming, the program which computes the sequence is like this:

 a[0] = 1;
    for (i = 1; i <= n; i = i+1)
        a[i] = 2*a[i-1]+2;

Then by using the solver, I can represent a[n] by n and add this feature to
constraint. However, I'm sort of finding the real world examples which
includes the recursive sequences or linear recurrence relation like this.
Do you know any piece of code which can be my test bench? I have searched
on coreutils and several benchmarks but found nothing relevant.

I also asked on Stackoverflow in this
topic<http://stackoverflow.com/questions/18203068/example-of-recursive-define-in-real-system-programs>.
Thank you for reading.
-- 
Loi, Luu The (Mr.)
RA at Security Lab, SoC, NUS
-------------- next part --------------
HTML attachment scrubbed and removed