A correctness proof of the bakery protocol in $ mu $CRL

Groote, Jan Friso; Korver, H.P.

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.

Additional Metadata
ACM	Specifying and Verifying and Reasoning about Programs (acm F.3.1)
MSC	Specification and verification (program logics, model checking, etc.) (msc 68Q60), Theorem proving (deduction, resolution, etc.) (msc 68T15)
Publisher	CWI
Series	Department of Computer Science [CS]
Organisation	Computer Systems & Telematics
Citation APA Style AAA Style APA Style Cell Style Chicago Style Harvard Style IEEE Style MLA Style Nature Style Vancouver Style American-Institute-of-Physics Style Council-of-Science-Editors Style BibTex Format Endnote Format RIS Format CSL Format DOIs only Format	Groote, J. F., & Korver, H. P. (1994). A correctness proof of the bakery protocol in $ mu $CRL. Department of Computer Science [CS]. CWI.

Free Full Text ( Final Version , 343kb )

A correctness proof of the bakery protocol in $ mu $CRL

Publication

Publication

Address

CWI researchers

Questions or comments?

A correctness proof of the bakery protocol in $ mu $CRL

Publication

Publication

Workflow

Workflow

Add Content