O. Travkin, H. Wehrheim, and G. Schellhorn, “Proving Linearizability of Multiset with Local Proof Obligations”, ECEASST, vol. 53, Jan. 2013.