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

[Martin Nowack]

Hi Chengyu,
> On 18 Nov 2016, at 15:16, Chengyu Zhang <dale.chengyu.zhang at gmail.com> wrote:
> 
>     But I have a question that why KLEE set uncovered-update interval default to 30 ticks rather than every time we do stepInstruction function?
>     Is it because of low efficiency or other reasons?
> 

Well, the current implementation is quite costly, therefore the high value of 30s.
This might be less of a problem with older machines but becomes more problematic with newer ones,
as they number of instructions per second might be much higher. So you update less often and might
work more often with outdated information.
So you should vary that number according to your needs.

(Of course, patches, which improve that situation are always welcome ;) )

Cheers,
Martin


> Best regards,
> Chengyu
> 
> 2016-11-02 18:00 GMT+08:00 Chengyu Zhang <dale.chengyu.zhang at gmail.com>:
> 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 
> 
> 
> 
> -- 
> 张枨宇   Chengyu Zhang
> East China Normal University 
> School of Computer Science and Software Engineering
> Tel: 18685412181
> Mail: dale.chengyu.zhang at gmail.com 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------