[klee-dev] Using klee for verification

[Kornilios Kourtis]

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