Association for Computing Machinery
Automated verification of distributed programs is a challenging problem. Since the behavior of a distributed program encompasses the behavior of the network, possible configurations of the network have to be investigated during verification. This leads to very large state spaces, and automated verification becomes infeasible. The authors present a framework that addresses this problem by decoupling the behavior of distributed programs from the behavior of the network. Their framework is based on a set of stub classes that replace native methods used in network communication and enables verification of distributed Java applications by isolating their behavior from the network.