[klee-dev] Path Search Heuristics

Zhiyi Zhang xianlingzibiying at gmail.com
Sun May 24 12:23:54 BST 2015


Hi all,

I have some questions about path search heuristics used in KLEE.

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?

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? Or Does it mean when one  search heuristic cannot find a
path during symbolic execution, then it uses the other  search heuristic to
find paths? If it is the later one, however, "nurs:covnew" can not be used
as only path search heuristic during symbolic execution.

Thank you!
Zhiyi Zhang
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list