Symbolic Execution of Distributed Systems

Automatism and high coverage are the core challenges in testing distributed systems in their early development phase. Ideally, the testing process should cope with a large input space, non-determinism, concurrency, and heterogeneous operating environments to effectively explore the behavior of unmodified software. In practice, however, missing tool support imposes significant manual effort to perform such integrated testing. Recent advances in symbolic execution have proposed a number of effective solutions to automatically achieve high code coverage and detect bugs in complex systems' software. Still, these approaches target at sequential programs and not their concurrent execution. Applying symbolic execution to distributed systems poses two core challenges: (1) scalability with network size and (2) state inter-dependencies resulting from communication involving symbolic data. This thesis presents symbolic distributed execution (SDE) -- a novel approach enabling symbolic execution of distributed systems. First, we generalize the problem space of SDE and enhance symbolic execution for distributed software analysis. Second, we significantly optimize the basic execution model of SDE by eliminating redundant execution paths. The key idea is to benefit from the nodes' local communication to minimize the number of states that represent a distributed execution. Third, we demonstrate the practical applicability and effectiveness of SDE with two integrated testing environments for real-world networked software.