[klee-dev] About KLEE

[Sean Bartell]

eric.rizzi at huskers.unl.edu on 2015-05-30:
>I'm not sure that what you are looking for exists. Klee is designed to test 
>programs and create test suites. It will find assertion violations and other 
>common errors. If you're looking to verify that a particular path through the 
>program is semantically correct, however, you're going to have to find some 
>type of specification for each program.   From that point, you could use the 
>inputs/ouputs generated by Klee to make sure they all match the 
>specifications.  As I said, however, I don't know where you will be able to 
>find any formal specifications for core-utils.
>
>
>The only option I can think of is to use some competing implementation of the core-utils and verify that they each produce the same outputs given the same inputs.

That reminds me, the [original KLEE 
paper](http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf) crosschecked 
Coreutils against Busybox (section 5.5). It's not the same as an oracle, 
though, and it will have lots of false positives due to different feature sets.
I'm not sure whether their "infrastructure to make crosschecking automatic" is 
open source.
-------------- next part --------------
HTML attachment scrubbed and removed