[klee-dev] Using klee for verification

[Jianxiong Gao]

Hi,

I believe the answer is yes and we have been using KLEE for verification
for years.
It indeed catches all the out-of-bound errors and that is one of the
several common
issues we catch.

Thanks
Gao

On Tue, Nov 13, 2018 at 7:37 AM Kornilios Kourtis <kornilios at gmail.com>
wrote:

> Hi,
>
> I've been playing around with klee, and so far it seems like a great tool!
>
> One thing I'm wondering is whether it can be used for verification
> (I'm thinking small pieces of code here). For example, in principle
> (ignoring potential klee code bugs) will klee _always_ report errors
> on code with out-of-bounds accesses? From a quick look at the code,
> the answer seems to be "yes", because whenever klee compromises it
> reports an error or warning. On the other hand, I have not seen such a
> use-case mentioned, so maybe I'm missing something.
>
> Thanks,
> Kornilios.
>
> --
> Kornilios Kourtis
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed