[klee-dev] Path Search Heuristics

[gwpublic at wp.pl]

It's explained in paper,

Also for exercise I recommend you to try to explore graph of possible
states of few simple programs (some execution path leading to infinite
loop, recursion) and you should see where things can keep exploring
indifinitely.

All the best!
Greg
On 25 May 2015 07:42, "Zhiyi Zhang" <xianlingzibiying at gmail.com> wrote:

> Hi Bartell,
>
> Thanks for your reply very much.
>
> 1, KLEE keeps running without printing anything. I set KLEE running time
> for one hour, but it stops very quickly. There is no error reports. In the
> klee-out folder, there are only "assembly.ll" and "run.stats" files.
> However, when I used bfs, dfs, random or nurs:depth, KLEE runs OK.
>
> 2, Why KLEE uses "interleaved" searcher? Is "interleaved" search heuristic
> better than single search heuristic for symbolic execution?
>
> Best wishes!
> Zhiyi Zhang,
>
> On Mon, May 25, 2015 at 5:20 AM, Sean Bartell <sean at yotann.org> wrote:
>
>>  Zhiyi Zhang on 2015-05-24:
>>
>> 1, It seems that KLEE can NOT generate test cases when I only used
>> search==nurs:covnew as the path search heuristic. Moreover, when using
>> search==nurs:md2u, search==nurs:icnt, search==nurs:cpicnt or
>> search==nurs:qc as as the only path search heuristic, KLEE also does NOT
>> generate test cases. I am confused why this phenomenon happens?
>>
>> How does it fail? Does it crash with an error message, or does it just
>> keep running without printing anything?
>>
>> 2, The default search heuristic for KLEE is "random-path interleaved with
>> nurs:covnew". What is the meaning of "interleaved"? Does it mean randomly
>> selecting one search heuristic from such two search heuristics when
>> searching a path?
>>
>> Yes, except that it isn't random. The "interleaved" searcher just
>> alternates between using two other searchers. "nurs:covnew" and other
>> searchers can always choose a state.
>>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
-------------- next part --------------
HTML attachment scrubbed and removed