ICE-TCS seminar: Huimin Lin (Chinese Academy of Sciences)
Date/Time: Monday, 23 May 2016, 11:00-12:00
Location: M1.02 - Reykjavík University
Speaker: Huimin Lin (Chinese Academy of Sciences, Beijing, China)
Title: Proving Linearizability via Branching Bisimulation
Abstract: Linearizability and progress properties are key correctness notions for concurrent
data structures. However, model checking linearizability has suffered from the
PSPACE-hardness of the trace inclusion problem. We propose to exploit branching
bisimulation, a fundamental semantic equivalence relation developed for process algebras,
in checking these properties. A quotient construction is provided which results in
huge state space reductions. The advantages of the proposed approach has been confirmed
on benchmark problems.
Joint work with Xiaoxiao Yang, Joost-Pieter Katoen and Hao Wu.