Cloud9 is a parallel symbolic execution engine that scales on shared-nothing clusters of commodity hardware. It can test systems ranging from command line utilities to Internet servers and distributed systems, thanks to its support for a symbolic POSIX OS environment. Cloud9 builds upon the KLEE symbolic execution engine. For more details about the principles behind Cloud9 and the applications it enables, check out the publication list.
Note: The version of Cloud9 that supports efficient state merging (PLDI'12) is available as a separate download: code & data. We plan to merge the code to mainstream Cloud9 in the future.