[klee-dev] Distributed Symbolic Execution

[emil.rakadjiev.bf at hitachi.com]

Hello,

I am involved in a project that aims to develop a scalable symbolic 
execution (KLEE) based testing tool. I have already done background 
research and tested KLEE and Cloud9, and I'm in the process of getting 
more familiar with the internal functionality and the code bases, and 
deciding in which direction to continue. I have a few preliminary questions:

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)?
2) In the context of question 1, what is your opinion about Cloud9's 
(higher-level) way of parallelizing KLEE?
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?

The first two questions are a bit broad, so I'm not expecting concrete 
answers, I would rather like to hear the opinions or gut feelings of 
people experienced with KLEE's architecture and symbolic execution. This 
would also help to go in a direction that could potentially be of 
benefit to KLEE, too.

Thank you!
Best regards,
Emil