[klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher

[Chengyu Zhang]

Hi all,

I saw the md2u(Min-Dist-to-Uncovered)  search heuristic in KLEE.
In my opinion, md2u is the strategy that when selecting a state KLEE aways
consider about
the states have the minimum distance to uncovered part of the code. I read
the source code
of the MinDistToUncovered, but I'm still confused about the implement of
computeMinDistToUncovered function.

So I have two questions:

1. If someone could give the algorithm description about how to compute the
minimum distance to uncovered part in KLEE or explain the implement of
computeMinDistToUncovered function in KLEE. And if I could compute the
distance between two instructions in KLEE.

2. What's the difference between CovNew and MD2U search heuristic ?

Thanks a lot.
Chengyu Zhang

-- 
张枨宇   Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: 18685412181
Mail: dale.chengyu.zhang at gmail.com
-------------- next part --------------
HTML attachment scrubbed and removed