[klee-dev] Why no BFS?

[Loi Luu]

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.
-------------- next part --------------
HTML attachment scrubbed and removed