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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
