[klee-dev] Distributed Symbolic Execution

[Cristian Cadar]

On 20/08/14 02:00, emil.rakadjiev.bf at hitachi.com wrote:
> 1) On the KLEE website, under the "Open Projects" section, you list
> "Distributed Constraint Solving" as one possible improvement. Since
> constraint solving dominates the run time of KLEE, it makes sense that
> this is the hottest target to parallelize. Based on your experience, do
> you imagine a good scalable KLEE implementation to be one that targets
> mainly/only parallel constraint solving? Also, do you think this is
> feasible on KLEE-level, without modifying the underlying constraint
> solver (and thereby restricting ourselves to one specific solver)?
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.

> 3) Cloud9 is based on KLEE, and besides distributed execution, it
> provides further improvements like an extended POSIX model, incl.
> multi-thread/process support. What is the reason that (part of) these
> improvements have not been merged into KLEE?
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.

Best,
Cristian