The Bakery Protocol: A Comparative Case-Study in Formal Verification

Abstract

Groote and the second author verified (a version of) the Bakery Protocol in μCRL. Their process-algebraic verification is rather complex compared to the protocol. Now the question is: How do other verification techniques perform on this protocol? In this paper we present a new correctness proof by using I/O-automata theory and discuss the relative merits of both approaches.