Towards an automatic proof of the bakery algorithm

DOI10.1007/978-3-031-35355-0_2zbMATH Open1543.68211MaRDI QIDQ6535458FDOQ6535458

Authors: Aman Goel, Stephan Merz, Karem A. Sakallah 

Publication date: 11 January 2024

Recommendations

• Nonatomic dual bakery algorithm with bounded tokens
• Correctness and concurrent complexity of the black-white bakery algorithm
• scientific article; zbMATH DE number 868108
• scientific article; zbMATH DE number 2080925
• Under the hood of the bakery algorithm: mutual exclusion as a matter of priority

zbMATH Keywords

mutual exclusionparameterized verificationinductive invariant

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Distributed algorithms (68W15) Distributed systems (68M14) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Algorithms for computing minimal unsatisfiable subsets of constraints
• On interprocess communication. I: Basic formalism
• Title not available (Why is that?)
• SAT-Based Model Checking without Unrolling
• Time, clocks, and the ordering of events in a distributed system
• A new solution of Dijkstra's concurrent programming problem
• TLA +  Proofs

This page was built for publication: Towards an automatic proof of the bakery algorithm

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535458)