ICE-TCS seminar: Huimin Lin (Chinese Academy of Sciences)

  • 23.5.2016, 11:00 - 12:00


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.

This talk is part of the ICE-TCS Theory Week, which will be concluded by the annual ICE-TCS Theory Day on Friday, 27 May.