[klee-dev] Distributed Symbolic Execution

[Emil Rakadjiev]

Hello Cristian,

> One thing that we have already tried out is to use multiple constraint 
> solvers, take a look here 
> http://srg.doc.ic.ac.uk/projects/klee-multisolver/.  So KLEE is not 
> restricted to a single solver anymore, although STP still seems to 
> generally perform the best, at least based on our (limited) experience.

Thanks for the reply! The multisolver/portfolio approach is definitely 
interesting, but with it the overall performance is still bounded by the 
performance of the fastest solver. That is, it improves symbolic 
execution performance, but it doesn't make it scalable. Our initial aim 
is similar to that of Cloud9, i.e. to have an implementation that can 
easily scale out, thus making it possible to test large applications and 
achieve higher coverage in a shorter amount of time.

> I think that's a better question to ask the Cloud9 developers :)  In 
> general, there are many nice tools out there that are based on KLEE, 
> and it is indeed unfortunate that they are not part of a single tool.  
> I strongly encourage people to contribute their techniques to KLEE, 
> and we've also tried to integrate more of our research work into the 
> main codebase (the multi-solver example mentioned above is one example).
>
> But at the same time I do understand that it is not always possible to 
> easily integrate things into KLEE's main codebase, often for 
> logistical reasons and time constraints.  From my conversation a while 
> ago with Stefan from Cloud9, I understand time is really the main 
> reason.  And now that the KLEE codebase has seen significant changes 
> in the last few years, this would be even more difficult.

Thank you for those details! I agree that it would be great to make KLEE 
even more versatile and possibly "production-ready" with the help of 
external contributions. But time indeed causes lots of inconvenience 
(... I've heard...).
The distributed execution part of Cloud9 introduces many changes to the 
code, so that would be harder to merge, but I was mainly surprised why 
the extended POSIX model has not been contributed to KLEE. Of course, 
multi-threading support also requires changes like extending states, 
adding scheduling, etc., and e.g. replaying thread interleavings is not 
trivial, but I think those additions from Cloud9 would be very useful 
for KLEE, too. Actually, this is something I was planning to look into, 
whether those extensions can be cleanly integrated into upstream KLEE. 
Unfortunately, Cloud9 doesn't seem to be maintained anymore.

Best regards,
Emil