[klee-dev] Whats the difference between RandomSearcher and RandomPathSearcher?

Sean Bartell sean at yotann.org
Mon Oct 12 22:14:23 BST 2015


Zaman, Tarannum on 2015-10-12:
>What I have understand that RandomSearcher selects next state randomly. But
>what actually the  RandomPathSearcher in Klee is doing? How it selects its
>next state and what is the difference between this two searcher?

Suppose KLEE has 3 states: one where the path is False (at first branch), one 
where the path is True (at first branch), False (at second branch), and one 
where the path is True (at first branch), True (at second branch). 

RandomSearcher gives each state a 1/3 probability, but there are two states 
starting with True and only one state starting with False, so there's a 2/3 
probability of choosing a state that starts with True. So it's fair between the 
states, but it's unfair between the paths in some sense.

RandomPathSearcher starts at the root and chooses a random direction at each 
branch with equal probability. It keeps going until it finds a state. So it has 
a 0.5 probability of choosing False and selecting the False state; if it 
chooses True, it makes another random choice for the second branch, so in total 
it has a 0.25 probability of choosing the True, False state and the same for 
the True, True state. So RandomPathSearcher is unfair between the states, but 
it's fair between the paths.
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list