In this quick tutorial, we will use Cloud9 to test a small C program that simulates a producer-consumer system. The system consists of a client process that produces a set of integer values, which are then sent to a consumer process. The producer instructs the consumer to terminate by sending a negative value at the end. The program makes use of the POSIX pthreads API, it forks processes, and does network communication, so we will use Cloud9's POSIX model to run it.
Cloud9 should complete execution within a few seconds, and output messages indicating the values that were produced/consumed, together with network state information (created sockets, initiated connections, etc.). The example program uses symbolic execution to a small extent. The producer marks as symbolic the last value to send to the consumer, and assumes that the value is negative, so the consumer would terminate.
That was quick, right? From this point, you can try testing other programs (memcached, Apache, Chromium's OpenType Sanitizer), and learn how to build LLVM binaries for your own testing targets.