A concurrent module provides procedures that may be invoked concurrently by its clients. We consider concurrent modules that utilize locking protocols, such as two-phase locking (2PL) or tree locking (TL), to guarantee serializability. We present analyses for verifying that a given module satisfies TL/2PL. Such analyses are useful as serializability is a desirable property of interest to the end user (programmer). 
However, there is another compelling factor that motivates us to pursue these analysis problems: if a concurrent module is verified to be serializable, then we can exploit this fact to perform other analyses of the module, e.g., verifying the absence of memory errors in the module, more efficiently and more precisely, by considering only serial executions of its procedures. 
This approach (to using sequential reasoning for subsequent analyses) becomes less attractive if the verification of serializability itself requires reasoning explicitly about all possible interleaved executions of the module's procedures. 

One of our main results is that the verification of the locking protocols (TL/2PL) can itself be done using a sequential analysis. We, in fact, prove this result for any locking protocol that satisfies certain reasonable conditions. Another contribution of this paper is that we present a couple of approaches to performing a sequential analysis of a concurrent module, and study the correctness conditions required by these approaches. One interesting outcome of this study is that one natural approach to sequential analysis actually requires a termination analysis for correctness.