Some bisimulation based abstract equivalence relations may equate divergent systems with non-divergent ones, examples including weak bisimulation equivalence and branching bisimulation equivalence. Thus extra efforts are needed to analyze divergence for the compared systems. In this paper we propose a new method for analyzing divergence in bisimulation semantics, which relies only on simple observations of individual transitions. We show that this method can verify several typical divergence preserving bisimulation equivalences including two well-known ones. As an application case study, we use the proposed method to verify the HSY collision stack to draw the conclusion that the stack implementation is correct in terms of linearizability with lock-free progress condition.
Fri 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00
|Parallel Functional Arrays|
|A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms|
|Analyzing divergence in bisimulation semantics|
|Fencing off Go: Liveness and Safety for Channel-Based Programming|
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UKPre-print