This paper presents our experiences in applying the Java PathFinder (Jpf), a recently developed Java to Promela translator,
in the search for synchronization bugs in a Chinese Chess game server application written in Java. We give an overview of
Jpf and the subset of Java that it supports and describe an initial effort to abstract and analyze the game server. Finally,
we evaluate the results of the effort.