[klee-dev] Why no BFS?

[Loi Luu]

Hello Paul,

I got this one:

| Path      | Instrs   | Time(s) | ICov(%) | BCov(%) | ICount | TSolver(%)
| States | maxStates | avgStates | Mem(MB) | maxMem(MB) | avgMem(MB) |
Queries | AvgQC | Tcex(%) | Tfork(%) |
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-last |  15428 |    0.03  |    7.12    |    4.24   |  29019  |
2.36    |      0   |         0       |      0.00    |   26.62 |      26.62
              |      26.47      |       1  |    15      |    2.19    |
0.00 |

This is still not as good as BFS result. And I want to emphasis again the
question is why no BFS?

Thanks,



On Tue, Apr 23, 2013 at 6:33 PM, Paul Marinescu <
paul.marinescu at imperial.ac.uk> wrote:

> 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<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>>
>>
>
> ______________________________**_________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
>



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