We use the verification system PVS to obtain mechanized support for the
formal verification of concurrency control protocols, concentrating on
A method to verify conflict serializability of transactions has been formulated in PVS and proved to be sound and complete with the interactive proof checker of this tool. The method has been used to verify a few basic protocols. Next we present a systematic way to extend these protocols with new actions and control information.
As another application, we discuss the formal specification and mechanical verification of a non-blocking atomic commitment protocol of Babaoglu and Toueg. An error has been found in the original termination part of the protocol and we have verified the correctness of our own improved protocol with PVS.