Hi Andy, the answer to the first two questions is a qualified yes -- you
can make these guarantees assuming no interaction with external code, no
constraint solving timeouts, no bugs in KLEE, etc. As to your final
question, there are several research projects that aim to do this (e.g.,
Hi, I have two questions which seem vaguely related:
1) If I run "klee foo.bc" and wait for it to finish, and it generates a bunch
of test vectors, then what guarantees can I make about that set of test vectors?
- Can I guarantee that all possible lines of code (or basic blocks) which can
be
