Accurate Centralization for Applying Model Checking on Networked Applications

Software model checkers can be applied directly to single-process programs, which typically are multithreaded. Multi-process applications cannot be model checked directly. While multiple processes can be merged manually into a single one, this process is very laborintensive and a major obstacle towards model checking of client-server applications. Previous work has automated the merging of multiple applications but mostly omitted network communication. Remote procedure calls were simply inlined, creating similar results for simple cases while removing much of the inherent complexities involved. Our goal is a fully transparent replacement of network communication. Other language features were also modeled more precisely than in previous work, resulting in a program that is much closer to the original. This makes our approach suitable for testing, debugging, and software model checking. Due to the increased faithfulness of our approach, we can treat a much larger range of applications than before.