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.zh...@gmail.com
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to