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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
