[klee-dev] Why no BFS?

[Paul Marinescu]

Hello Loi,
DFS is not the default searcher for a few months now. What results do 
you get with no --search argument?

Paul

On 23/04/13 12:03, Loi Luu wrote:
> Dear all,
>
> I just added bfs-searcher to klee and make some comparisons between DFS
> (which is default searcher now) and BFS. Surprisingly, the result for
> branch coverage and instruction coverage of BFS are better in some cases
> and equally good in almost all cases than that of DFS.
>
> For example, in the *stat *in coreutils 6.11:
> with --search=bfs
> | Path          | Instrs   | Time(s) | ICov(%) | BCov(%) | ICount |
> TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
> avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
> ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
> | klee-out-10 |  21801 |    0.04   |   15.34 |    9.99     |  29019 |
>      1.49    |      0    |         0         |      0.00 |   26.64
>   |      26.64        |         26.47             |       1 |    15
>    |    1.37    |     0.00 |
>
> with --search=dfs
>
> | Path          | Instrs   | Time(s) | ICov(%) | BCov(%) | ICount |
> TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
> avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
> --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
> | klee-last     |  15356 |    0.03   |    7.12  |    4.24     |  29019 |
>        1.90    |      0    |         0      |      0.00    |   26.61
> |      26.61     |      26.46               |       1   |    15      |
>   1.75  |     0.00 |
>
>
> The difference of state space is pretty small, so is there any reason
> that BFS is not included in Klee?
>
> Thanks,
> --
> Loi, Luu The (Mr.)
> University of  Engineering and Technology, Vietnam National University,
> Hanoi.
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>