Just verification of mutual exclusion algorithms

DOI10.4230/LIPICS.CONCUR.2025.17MaRDI QIDQ7310288zbMATH OpenFDO

Authors Rob van Glabbeek, Bas Luttik, Myrthe S. C. Spronck

Publication date 5 August 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2025.17

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• A fine-grained solution to the mutual exclusion problem
• A new solution of Dijkstra's concurrent programming problem
• A New Solution to Lamport's Concurrent Programming Problem Using Small Shared Variables
• Analysing mutual exclusion using process algebra with signals
• Arbitration without common modifiable variables
• Bounds on shared memory for mutual exclusion
• Concurrent programming: algorithms, principles, and foundations.
• Formal Methods for the Design of Real-Time Systems
• Handling Parameterized Systems with Non-atomic Global Conditions
• scientific article; zbMATH DE number 1670791 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 2081102 (Why is no real title available?)
• Justness. A completeness criterion for capturing liveness properties (extended abstract)
• Laws of order, expensive synchronization in concurrent algorithms cannot be eliminated
• Model checking and abstraction to the aid of parameterized systems (a survey)
• Modeling and analysis of communicating systems
• Modelling mutual exclusion in a process algebra with time-outs
• Multiwriter consistency conditions for shared memory registers
• Myths about the mutual exclusion problem
• Nonatomic dual bakery algorithm with bounded tokens
• Off-the-shelf automated analysis of liveness properties for just paths
• On interprocess communication. I: Basic formalism
• On interprocess communication. II: Algorithms
• Principles of the SPIN model checker. Foreword by Gerard J. Holzmann
• Process-algebraic models of multi-writer multi-reader non-atomic registers
• Progress, justness and fairness in modal -calculus formulae
• Proof rules and transformations dealing with fairness
• The mutual exclusion problem
• The mutual exclusion problem
• Time and Fairness in a Process Algebra with Non-blocking Reading

This page was built for publication: Just verification of mutual exclusion algorithms

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