@article(abadi,
 author       = {M. Abadi and L. Lamport},
 year         = {1991},
 title        = {The existence of refinement mappings},
 journal      = {Theoretical Computer Science},
 volume       = {82},
 number       = {2},
 pages        = {253--284},
 doi          = {10.1016/0304-3975(91)90224-P},
)
@article(Alglave:2014:HCM:2633904.2627752,
 author       = {J. Alglave and L. Maranget and M. Tautschnig},
 year         = {2014},
 title        = {Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {36},
 number       = {2},
 pages        = {7:1--7:74},
 doi          = {10.1145/2627752},
)
@inproceedings(back,
 author       = {R.-J.R. Back},
 year         = {1990},
 title        = {Refinement calculus, part {II}: Parallel and reactive programs},
 booktitle    = {Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness},
 organization = {Springer},
 pages        = {67--93},
 doi          = {10.1007/3-540-52559-9\unhbox\voidb@x \vbox{\hrule width0.4em}60},
)
@inproceedings(bac94a,
 author       = {R.-J.R. Back and J. von Wright},
 year         = {1994},
 title        = {Trace refinement of action systems},
 booktitle    = {CONCUR '94},
 series       = {LNCS},
 volume       = {836},
 publisher    = {Springer},
 pages        = {367--384},
 doi          = {10.1007/978-3-540-48654-1\unhbox\voidb@x \vbox{\hrule width0.4em}28},
)
@incollection(bur12,
 author       = {S. Burckhardt and A. Gotsman and M. Musuvathi and H. Yang},
 year         = {2012},
 title        = {Concurrent Library Correctness on the {TSO} Memory Model},
 editor       = {H. Seidl},
 booktitle    = {ESOP 2012},
 series       = {LNCS},
 volume       = {7211},
 publisher    = {Springer},
 pages        = {87--107},
 doi          = {10.1007/978-3-642-28869-2\unhbox\voidb@x \vbox{\hrule width0.4em}5},
)
@inproceedings(ColvinFM2018,
 author       = {R.J. Colvin and G. Smith},
 year         = {2018},
 title        = {A wide-spectrum language for verification of programs on weak memory models},
 editor       = {K. Havelund and J. Peleska and B. Roscoe and E. de Vink},
 booktitle    = {{FM 2018}},
 series       = {LNCS},
 volume       = {10951},
 publisher    = {Springer},
 pages        = {240--257},
 doi          = {10.1007/978-3-319-95582-7\unhbox\voidb@x \vbox{\hrule width0.4em}14},
)
@inproceedings(ifm,
 author       = {J. Derrick and G. Smith and B. Dongol},
 year         = {2014},
 title        = {Verifying linearizability on {TSO} architectures},
 editor       = {E. Albert and E. Sekerinski},
 booktitle    = {iFM 2014},
 series       = {LNCS},
 volume       = {8739},
 publisher    = {Springer},
 pages        = {341--356},
 doi          = {10.1007/978-3-319-10181-1\unhbox\voidb@x \vbox{\hrule width0.4em}21},
)
@inproceedings(DohertyDerrick2016,
 author       = {S. Doherty and J. Derrick},
 year         = {2016},
 title        = {Linearizability and Causality},
 booktitle    = {SEFM 2016},
 series       = {LNCS},
 volume       = {9763},
 publisher    = {Springer},
 pages        = {45--60},
 doi          = {10.1007/978-3-319-41591-8\unhbox\voidb@x \vbox{\hrule width0.4em}4},
)
@inproceedings(Dongol2016,
 author       = {B. Dongol and L. Groves},
 year         = {2016},
 title        = {Contextual Trace Refinement for Concurrent Objects: Safety and Progress},
 editor       = {K. Ogata and M. Lawford and S. Liu},
 booktitle    = {ICFEM 2016},
 publisher    = {Springer},
 pages        = {261--278},
 doi          = {10.1007/978-3-319-47846-3\unhbox\voidb@x \vbox{\hrule width0.4em}17},
)
@inproceedings(DongolVMCAI2018,
 author       = {B. Dongol and R. Jagadeesan and J. Riely and A. Armstrong},
 year         = {2018},
 title        = {On abstraction and compositionality for weak-memory linearisability},
 editor       = {I. Dillig and J. Palsberg},
 booktitle    = {{VMCAI}'18},
 series       = {LNCS},
 volume       = {10747},
 publisher    = {Springer},
 pages        = {183--204},
 doi          = {10.1007/978-3-319-73721-8\unhbox\voidb@x \vbox{\hrule width0.4em}9},
)
@article(Filipovic-LinvsRef2010,
 author       = {I. Filipovi\'c and P. W. O'Hearn and N. Rinetzky and H. Yang},
 year         = {2010},
 title        = {Abstraction for concurrent objects},
 journal      = {Theoretical Computer Science},
 volume       = {411},
 number       = {51-52},
 pages        = {4379 -- 4398},
 doi          = {10.1016/j.tcs.2010.09.021},
)
@inproceedings(armv8,
 author       = {S. Flur and K.E. Gray and C. Pulte and S. Sarkar and A. Sezgin and L. Maranget and W. Deacon and P. Sewell},
 year         = {2016},
 title        = {Modelling the {ARMv8} Architecture, Operationally: Concurrency and {ISA}},
 editor       = {R. Bodik and R. Majumdar},
 booktitle    = {POPL 2016},
 publisher    = {ACM},
 pages        = {608--621},
 doi          = {10.1145/2837614.2837615},
)
@incollection(got12,
 author       = {A. Gotsman and M. Musuvathi and H. Yang},
 year         = {2012},
 title        = {Show No Weakness: Sequentially Consistent Specifications of {TSO} Libraries},
 editor       = {M. Aguilera},
 booktitle    = {DISC 2012},
 series       = {LNCS},
 volume       = {7611},
 publisher    = {Springer},
 pages        = {31--45},
 doi          = {10.1007/978-3-642-28869-2\unhbox\voidb@x \vbox{\hrule width0.4em}5},
)
@inproceedings(GotsmanYang2011,
 author       = {A. Gotsman and H. Yang},
 year         = {2011},
 title        = {Liveness-preserving atomicity abstraction},
 booktitle    = {ICALP 2011},
 series       = {LNCS},
 volume       = {6756},
 publisher    = {Springer},
 pages        = {453--465},
 doi          = {10.1007/978-3-642-22012-8\unhbox\voidb@x \vbox{\hrule width0.4em}36},
)
@article(HeWi90,
 author       = {M. 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(Moi07,
 author       = {M. Moir and N. Shavit},
 year         = {2004},
 title        = {Concurrent data structures},
 journal      = {Handbook of Data Structures and Applications},
 pages        = {47:1--47:30},
 doi          = {10.1201/9781420035179.ch47},
)
@inproceedings(Owens2009,
 author       = {S. Owens and S. Sarkar and P. Sewell},
 year         = {2009},
 title        = {A Better x86 Memory Model: x86-TSO},
 editor       = {S. Berghofer and T. Nipkow and C. Urban and M. Wenzel},
 booktitle    = {{TPHOLs} 2009},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {391--407},
 doi          = {10.1007/978-3-642-03359-9\unhbox\voidb@x \vbox{\hrule width0.4em}27},
)
@article(Sewell:2010:XRU:1785414.1785443,
 author       = {P. Sewell and S. Sarkar and S. Owens and F.Z. Nardelli and M.O. Myreen},
 year         = {2010},
 title        = {{x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors}},
 journal      = {Commun. ACM},
 volume       = {53},
 number       = {7},
 pages        = {89--97},
 doi          = {10.1145/1785414.1785443},
)
@article(Smith2017,
 author       = {G. Smith and K. Winter},
 year         = {2017},
 title        = {Relating trace refinement and linearizability},
 journal      = {Formal Aspects of Computing},
 volume       = {29},
 number       = {6},
 pages        = {935--950},
 doi          = {10.1007/s00165-017-0418-2},
)
@inproceedings(DBLP:conf/hvc/TravkinMW13,
 author       = {O. Travkin and A. M{\"u}tze and H. Wehrheim},
 year         = {2013},
 title        = {{SPIN} as a Linearizability Checker under Weak Memory Models},
 editor       = {V. Bertacco and A. Legay},
 booktitle    = {HVC2013},
 series       = {LNCS},
 volume       = {8244},
 publisher    = {Springer},
 pages        = {311--326},
 doi          = {10.1007/978-3-319-03077-7\unhbox\voidb@x \vbox{\hrule width0.4em}21},
)