Deadlocks are a common type of faults in distributed programs. To detect deadlocks in a distributed program P one approach is to construct the reachability graph (RG) of P which contains all possible states of P Since the size of RG (P) is an exponential function of the number of processes in P the use of RGs for deadlock detection has limted success.

In this paper, we show an efficient technique for deadlock analysis of client/server programs with two-way communication, where the server and clients ommunicate through channels supporting synchronous message-passing. We consider client/server programs in which the server saves the IDs of some lients for future communication. For such a program, we describe how to construct its abstract client/server reachability graph (ACSRG), which contains significantly less number of global states than the corresponding RG. One example is that for a solution to the gas station problem with one pump and six customers, its RG has 25394 states and its ACSRG 74 states. We showthat the use of ACSRGs not only greatly reduces the effort for deadlock analysis but also provides a basis for proving freedom from deadlocks for any number of lients.