Model Checking of Distributed Multi-Threaded Java Applications

In this dissertation, we focus on the verification of distributed Java applications composed of communicating multithreaded processes. We choose model checking as the verification technique. We propose an instance of the so-called centralization approach which allows for model checking multiple communicating processes. The main challenge of applying centralization is keeping data separated between different processes. In our approach, this issue is addressed through a new class-loading model. As one of our contributions, we implement our approach within an existing model checker, Java PathFinder (JPF). To account for interactions between processes, our approach provides the model checker with a model of interprocess communication. Moreover, our model allows for systematically exploring potential exceptional control flows caused by network failures. We also apply a partial order reduction (POR) algorithm to reduce the state space of distributed applications, and we prove that our POR algorithm preserves deadlocks. Furthermore, we propose an automatic approach to capture interactions between the system being verified and external resources, such as cloud computing services. The dissertation also discusses how our approach is superior to existing approaches. Our approach exhibits better performance which is mainly due to the POR technique. Furthermore, our approach allows for verifying a considerably larger class of applications without the need for any manual modeling, and it has been successfully used to detect bugs that cannot be found using previous work.