[klee-dev] Why there are so many weighted random search algorithms in KLEE?

Loi Luu loi.luuthe at gmail.com
Tue Apr 30 16:41:37 BST 2013


Hi Greg,

In file searcher.cpp, the selectState function is implemented as:

ExecutionState &WeightedRandomSearcher::selectState() {
  return *states->choose(theRNG.getDoubleL());
}

They just randomize a double number as the weight of the wanted state and
find it from the execution tree.

Regards,


On Tue, Apr 30, 2013 at 7:40 PM, <gwpublic at wp.pl> wrote:

> Hi Loi,
>
> As far as I remember from papers, it was NOT like taking any random
> not processed leafs, but some kind of mixture between bfs/dfs to avoid
> problems with loops. However I have not digged (yet) into that part of
> code, so it's hard to me to point specifics.
>
> Cheers,
> Greg
>
>
> On Tue, Apr 30, 2013 at 2:12 PM, Loi Luu <loi.luuthe at gmail.com> wrote:
> > Hi Greg,
> >
> > What I am curious is that when we select the state, we do it randomly.
> > Therefore, the effect of distribution type is reduced or maybe zero. So
> am I
> > right to think that?
> >
> > Regards,
> >
> >
> > On Tue, Apr 30, 2013 at 6:57 PM, <gwpublic at wp.pl> wrote:
> >>
> >> Hello,
> >>
> >> > I noticed that there are several NURS algorithms in klee, and each
> will
> >> > randomly select a state based on its own distribution. So why do we
> need
> >> > many of them in KLEE while after all we do randomly select states?
> >>
> >>
> >> For me it feels like you've answered your own question:
> >> Because they have different distributions :).
> >>
> >> If you would have findings about best distribution for selecting next
> >> node (maybe taking into account control/data flow structure) this
> >> might be nice contribution.
> >>
> >> Cheers,
> >> Greg
> >
> >
> >
> >
> > --
> > Loi, Luu The (Mr.)
> > University of  Engineering and Technology, Vietnam National University,
> > Hanoi.
>



-- 
Loi, Luu The (Mr.)
University of  Engineering and Technology, Vietnam National University,
Hanoi.
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list