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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Concurrency 3POPL at Amphitheater 44
Chair(s): Adam Chlipala MIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar , Guy E. Blelloch Carnegie Mellon University, Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
Igor Konnov TU Wien, Marijana Lazić TU Wien, Helmut Veith TU Wien, Josef Widder TU Wien
DOI Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin Liu Institute of software, Chinese academy of sciences, Tingting Yu , Wenhui Zhang Institute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print