@article(DongolD14-csur,
 author       = {B. Dongol and J. Derrick},
 year         = {2015},
 title        = {Verifying Linearisability: A Comparative Survey},
 journal      = {ACM Comput. Surv.},
 volume       = {48},
 number       = {2},
 pages        = {19:1--19:43},
 doi          = {10.1145/2796550},
)
@inproceedings(DDGS15-ECOOP,
 author       = {B. Dongol and J. Derrick and L. Groves and G. Smith},
 year         = {2015},
 title        = {Defining Correctness Conditions for Concurrent Objects in Multicore Architectures},
 editor       = {J. T. Boyland},
 booktitle    = {ECOOP},
 series       = {LIPIcs},
 volume       = {37},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {470--494},
 doi          = {10.4230/LIPIcs.ECOOP.2015.470},
)
@article(FORY10,
 author       = {I. Filipovic and P. W. O'Hearn and N. Rinetzky and H. Yang},
 year         = {2010},
 title        = {Abstraction for concurrent objects},
 journal      = {Theor. Comput. Sci.},
 volume       = {411},
 number       = {51-52},
 pages        = {4379--4398},
 doi          = {10.1016/j.tcs.2010.09.021},
)
@inproceedings(GY11,
 author       = {A. Gotsman and H. Yang},
 year         = {2011},
 title        = {Liveness-Preserving Atomicity Abstraction},
 editor       = {L. Aceto and M. Henzinger and J. Sgall},
 booktitle    = {ICALP(2)},
 series       = {LNCS},
 volume       = {6756},
 publisher    = {Springer},
 pages        = {453--465},
 doi          = {10.1007/978-3-642-22012-8\unhbox\voidb@x \kern0.06em\vbox{\hrule width0.5em}36},
)
@inproceedings(HDM10,
 author       = {I. J. Hayes and S. Dunne and L. Meinicke},
 year         = {2010},
 title        = {Unifying Theories of Programming That Distinguish Nontermination and Abort},
 editor       = {C. Bolduc and J. Desharnais and B. Ktari},
 booktitle    = {{MPC}},
 series       = {LNCS},
 volume       = {6120},
 publisher    = {Springer},
 pages        = {178--194},
 doi          = {10.1007/978-3-642-13321-3\unhbox\voidb@x \kern0.06em\vbox{\hrule width0.5em}12},
)
@inproceedings(HeHS86,
 author       = {J. He and C. A. R. Hoare and J. W. Sanders},
 year         = {1986},
 title        = {Data Refinement Refined},
 editor       = {B. Robinet and R. Wilhelm},
 booktitle    = {{ESOP}},
 series       = {LNCS},
 volume       = {213},
 publisher    = {Springer},
 pages        = {187--196},
 doi          = {10.1007/3-540-16442-1\unhbox\voidb@x \kern0.06em\vbox{\hrule width0.5em}14},
)
@book(HeSh08,
 author       = {M. Herlihy and N. Shavit},
 year         = {2008},
 title        = {The Art of Multiprocessor Programming},
 publisher    = {Morgan Kaufmann},
)
@article(Herlihy90,
 author       = {M. P. Herlihy and J. M. Wing},
 year         = {1990},
 title        = {Linearizability: a correctness condition for concurrent objects},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {12},
 number       = {3},
 pages        = {463--492},
 doi          = {10.1145/78969.78972},
)
@article(Lam79,
 author       = {L. Lamport},
 year         = {1979},
 title        = {How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor},
 journal      = {IEEE Trans. Computers},
 volume       = {46},
 number       = {7},
 pages        = {779--782},
 doi          = {10.1109/12.599898},
)
@techreport(Tre86,
 author       = {R. K. Treiber},
 year         = {1986},
 title        = {Systems programming: {C}oping with parallelism},
 type         = {Technical Report},
 number       = {RJ 5118},
 institution  = {IBM Almaden Res. Ctr.},
)