JPF-NAS Extension of Java Pathfinder

Java PathFinder (JPF) version 7 provides basic support for verifying the distributed Java applications. It can receive a distributed Java application as input that is perceived as multiple Java processes. However, JPF does account for communication between processes of the distributed application, and it thus cannot be used to verify any realistic distributed Java application. Applying JPF on distributed applications requires a model of inter-process communication (IPC) and process aware scheduling.