1 Introduction

2 Linearizability

3 Verifying linearizability

4 Case study 1: An optimistic set algorithm

5 Case study 2: A lazy set algorithm

6 Case study 3: The Herlihy-Wing queue

7 Conclusions