A specification of a bakery protocol is given in $mu$CRL. We provide a simple correctness criterion for the protocol. Then the protocol is proven correct using a proof system that has been developed for $mu$CRL. The proof primarily consists of algebraic manipulations based on specifications of abstract data types and elementary rules and axioms from process algebra.

Department of Computer Science [CS]
Computer Systems & Telematics

Groote, J.F, & Korver, H.P. (1994). A correctness proof of the bakery protocol in $ mu $CRL. Department of Computer Science [CS]. CWI.