Transformations for Model Checking Distributed Java Programs
Scott D. Stoller and Yanhong A. Liu

This paper describes three program transformations that extend the scope of model checkers for Java programs to include distributed programs, i.e., multi-process programs. The transformations combine multiple processes into a single process, replace remote method invocations (RMIs) with local method invocations that simulate RMIs, and replace cryptographic operations with symbolic counterparts.