5 papers
On the Notions of Bounded Bypass, and How to Make any Deadlock-Free MUTEX Protocol Satisfy One of Them
Rob van Glabbeek, Daniele Gorla, Myrthe Spronck
In the literature on mutual exclusion, bounded bypass has been used for a long time as a strengthening of starvation-freedom, but, to the best of our knowledge, it still lacks a sa…
Just Verification of Mutual Exclusion Algorithms with (Non-)Blocking and (Non-)Atomic Registers
Rob van Glabbeek, Bas Luttik, Myrthe Spronck
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where th…
Just Verification of Mutual Exclusion Algorithms
Rob van Glabbeek, Bas Luttik, Myrthe Spronck
We verify the correctness of a variety of mutual exclusion algorithms through model checking. We look at algorithms where communication is via shared read/write registers, where th…
Progress, Justness and Fairness in Modal -Calculus Formulae
Myrthe Spronck, Bas Luttik, Tim Willemse
When verifying liveness properties on a transition system, it is often necessary to discard spurious violating paths by making assumptions on which paths represent realistic execut…
Process-Algebraic Models of Multi-Writer Multi-Reader Non-Atomic Registers
Myrthe Spronck, Bas Luttik
We present process-algebraic models of multi-writer multi-reader safe, regular and atomic registers. We establish the relationship between our models and alternative versions prese…