POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 15:10 - 15:35 at Amphitheater 44 - Concurrency 3 Chair(s): Adam Chlipala

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 Jan

14:20 - 16:00: POPL - Concurrency 3 at Amphitheater 44
Chair(s): Adam ChlipalaMIT
POPL-2017-papers14:20 - 14:45
Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper
POPL-2017-papers14:45 - 15:10
DOI Pre-print
POPL-2017-papers15:10 - 15:35
Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences
POPL-2017-papers15:35 - 16:00
Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK