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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Concurrency 3POPL at Amphitheater 44
Chair(s): Adam ChlipalaMIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
DOI Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK
Pre-print