Transformations for Model Checking Distributed Java Programs

Abstract. 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.

• Type: Conference
• Year: 2001
• Where: SPIN
• Authors: Scott D. Stoller, Yanhong A. Liu
• Keywords: Local Method Invocations, Method Invocations, Replace Remote Method, SPIN 2001, Theoretical Computer Science