[klee-dev] Path Search Heuristics

[Zhiyi Zhang]

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.
>
-------------- next part --------------
HTML attachment scrubbed and removed