eric.ri...@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.
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
