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

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)