Towards an automatic proof of the bakery algorithm

DOI10.1007/978-3-031-35355-0_2MaRDI QIDQ6535458zbMATH OpenFDO

Authors Aman Goel, Stephan Merz, Karem A. Sakallah

Publication date 11 January 2024

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)

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

Cites work

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

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)