short.bib

% This file was created with JabRef 2.10.
% Encoding: UTF8


@InProceedings{Abdulla:1993,
  Title                    = {Verifying Programs with Unreliable Channels},
  Author                   = {Parosh Aziz Abdulla and
 Bengt Jonsson},
  Booktitle                = {LICS},
  Year                     = {1993},
  Pages                    = {160-170},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/lics/LICS8, DBLP:conf/lics/1993},
  Ee                       = {http://dx.doi.org/10.1109/LICS.1993.287591}
}

@InProceedings{Kiran:2013,
  Title                    = {Verifying a Quantitative Relaxation of Linearizability via Refinement},
  Author                   = {Kiran Adhikari and
 James Street and
 Chao Wang and
 Yang Liu and
 Shao Jie Zhang},
  Booktitle                = {Model Checking Software - 20th International Symposium, {SPIN} 2013,
 Stony Brook, NY, USA, July 8-9, 2013. Proceedings},
  Year                     = {2013},
  Pages                    = {24--42},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/spin/AdhikariSWLZ13},
  Crossref                 = {DBLP:conf/spin/2013},
  Doi                      = {10.1007/978-3-642-39176-7_3},
  Timestamp                = {Tue, 09 Sep 2014 18:51:38 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-39176-7_3}
}

@InProceedings{Yehuda:2010,
  Title                    = {Quasi-Linearizability: Relaxed Consistency for Improved Concurrency},
  Author                   = {Yehuda Afek and
 Guy Korland and
 Eitan Yanovsky},
  Booktitle                = {Principles of Distributed Systems - 14th International Conference,
 {OPODIS} 2010, Tozeur, Tunisia, December 14-17, 2010. Proceedings},
  Year                     = {2010},
  Pages                    = {395--410},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/opodis/AfekKY10},
  Crossref                 = {DBLP:conf/opodis/2010},
  Doi                      = {10.1007/978-3-642-17653-1_29},
  Timestamp                = {Thu, 09 Dec 2010 16:08:12 +0100},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-17653-1_29}
}

@InProceedings{Daphna:2007,
  Title                    = {Comparison Under Abstraction for Verifying Linearizability},
  Author                   = {Daphna Amit and
 Noam Rinetzky and
 Thomas W. Reps and
 Mooly Sagiv and
 Eran Yahav},
  Booktitle                = {Computer Aided Verification, 19th International Conference, {CAV}
 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  Year                     = {2007},
  Pages                    = {477--490},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/cav/AmitRRSY07},
  Crossref                 = {DBLP:conf/cav/2007},
  Doi                      = {10.1007/978-3-540-73368-3_49},
  Timestamp                = {Mon, 03 Sep 2007 13:24:22 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-540-73368-3_49}
}

@InProceedings{Mohamed:2012,
  Title                    = {What's Decidable about Weak Memory Models?},
  Author                   = {Mohamed Faouzi Atig and
 Ahmed Bouajjani and
 Sebastian Burckhardt and
 Madanlal Musuvathi},
  Booktitle                = {ESOP},
  Year                     = {2012},
  Pages                    = {26-46},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/esop/2012},
  Ee                       = {http://dx.doi.org/10.1007/978-3-642-28869-2_2}
}

@InProceedings{Mark:2013,
  Title                    = {Library abstraction for C/C++ concurrency},
  Author                   = {Mark Batty and
 Mike Dodds and
 Alexey Gotsman},
  Booktitle                = {POPL},
  Year                     = {2013},
  Pages                    = {235-248},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/popl/2013},
  Ee                       = {http://doi.acm.org/10.1145/2429069.2429099}
}

@InProceedings{Josh:2008,
  Title                    = {Thread Quantification for Concurrent Shape Analysis},
  Author                   = {Josh Berdine and
 Tal Lev{-}Ami and
 Roman Manevich and
 G. Ramalingam and
 Shmuel Sagiv},
  Booktitle                = {Computer Aided Verification, 20th International Conference, {CAV}
 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
  Year                     = {2008},
  Pages                    = {399--413},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/cav/BerdineLMRS08},
  Crossref                 = {DBLP:conf/cav/2008},
  Doi                      = {10.1007/978-3-540-70545-1_37},
  Timestamp                = {Tue, 08 Jul 2008 14:46:07 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-540-70545-1_37}
}

@InProceedings{Bouajjani:2015,
  Title                    = {On Reducing Linearizability to State Reachability},
  Author                   = {Ahmed Bouajjani and
 Michael Emmi and
 Constantin Enea and
 Jad Hamza},
  Booktitle                = {Automata, Languages, and Programming - 42nd International Colloquium,
 {ICALP} 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part {II}},
  Year                     = {2015},
  Editor                   = {Magn{\'{u}}s M. Halld{\'{o}}rsson and
 Kazuo Iwama and
 Naoki Kobayashi and
 Bettina Speckmann},
  Pages                    = {95--107},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/icalp/BouajjaniEEH15},
  Crossref                 = {DBLP:conf/icalp/2015-2},
  Doi                      = {10.1007/978-3-662-47666-6_8},
  Timestamp                = {Mon, 22 Jun 2015 12:04:57 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-662-47666-6_8}
}

@InProceedings{Bouajjani:2015a,
  Title                    = {Tractable Refinement Checking for Concurrent Objects},
  Author                   = {Ahmed Bouajjani and
 Michael Emmi and
 Constantin Enea and
 Jad Hamza},
  Booktitle                = {Proceedings of the 42nd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
 Principles of Programming Languages, {POPL} 2015, Mumbai, India, January
 15-17, 2015},
  Year                     = {2015},
  Pages                    = {651--662},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/popl/BouajjaniEEH15},
  Crossref                 = {DBLP:conf/popl/2015},
  Doi                      = {10.1145/2676726.2677002},
  Timestamp                = {Sat, 20 Dec 2014 16:58:56 +0100},
  Url                      = {http://doi.acm.org/10.1145/2676726.2677002}
}

@InProceedings{Sebastian:2010,
  Title                    = {Line-up: a complete and automatic linearizability checker},
  Author                   = {Sebastian Burckhardt and
 Chris Dern and
 Madanlal Musuvathi and
 Roy Tan},
  Booktitle                = {Proceedings of the 2010 {ACM} {SIGPLAN} Conference on Programming
 Language Design and Implementation, {PLDI} 2010, Toronto, Ontario,
 Canada, June 5-10, 2010},
  Year                     = {2010},
  Pages                    = {330--340},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/pldi/BurckhardtDMT10},
  Crossref                 = {DBLP:conf/pldi/2010},
  Doi                      = {10.1145/1806596.1806634},
  Timestamp                = {Mon, 07 Jun 2010 09:41:55 +0200},
  Url                      = {http://doi.acm.org/10.1145/1806596.1806634}
}

@InProceedings{Sebastian:2012,
  Title                    = {Concurrent Library Correctness on the TSO Memory Model},
  Author                   = {Sebastian Burckhardt and
 Alexey Gotsman and
 Madanlal Musuvathi and
 Hongseok Yang},
  Booktitle                = {ESOP},
  Year                     = {2012},
  Pages                    = {87-107},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/esop/2012},
  Ee                       = {http://dx.doi.org/10.1007/978-3-642-28869-2_5}
}

@InProceedings{John:2007,
  Title                    = {Proving Linearizability Via Non-atomic Refinement},
  Author                   = {John Derrick and
 Gerhard Schellhorn and
 Heike Wehrheim},
  Booktitle                = {Integrated Formal Methods, 6th International Conference, {IFM} 2007,
 Oxford, UK, July 2-5, 2007, Proceedings},
  Year                     = {2007},
  Pages                    = {195--214},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/ifm/DerrickSW07},
  Crossref                 = {DBLP:conf/ifm/2007},
  Doi                      = {10.1007/978-3-540-73210-5_11},
  Timestamp                = {Thu, 20 Sep 2007 12:05:32 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-540-73210-5_11}
}

@InProceedings{John:2005,
  Title                    = {Non-atomic Refinement in {Z} and {CSP}},
  Author                   = {John Derrick and
 Heike Wehrheim},
  Booktitle                = {{ZB} 2005: Formal Specification and Development in {Z} and B, 4th
 International Conference of {B} and {Z} Users, Guildford, UK, April
 13-15, 2005, Proceedings},
  Year                     = {2005},
  Pages                    = {24--44},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/zum/DerrickW05},
  Crossref                 = {DBLP:conf/zum/2005},
  Doi                      = {10.1007/11415787_3},
  Timestamp                = {Mon, 13 Mar 2006 09:07:14 +0100},
  Url                      = {http://dx.doi.org/10.1007/11415787_3}
}

@InProceedings{Simon:2004,
  Title                    = {Formal Verification of a Practical Lock-Free Queue Algorithm},
  Author                   = {Simon Doherty and
 Lindsay Groves and
 Victor Luchangco and
 Mark Moir},
  Booktitle                = {Formal Techniques for Networked and Distributed Systems - {FORTE}
 2004, 24th {IFIP} {WG} 6.1 International Conference, Madrid Spain,
 September 27-30, 2004, Proceedings},
  Year                     = {2004},
  Pages                    = {97--114},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/forte/DohertyGLM04},
  Crossref                 = {DBLP:conf/forte/2004},
  Doi                      = {10.1007/978-3-540-30232-2_7},
  Timestamp                = {Wed, 10 Aug 2011 18:00:06 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-540-30232-2_7}
}

@InProceedings{Ivana:2009,
  Title                    = {Abstraction for Concurrent Objects},
  Author                   = {Ivana Filipovic and
 Peter W. O'Hearn and
 Noam Rinetzky and
 Hongseok Yang},
  Booktitle                = {ESOP},
  Year                     = {2009},
  Pages                    = {252-266},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/esop/2009},
  Ee                       = {http://dx.doi.org/10.1007/978-3-642-00590-9_19}
}

@InProceedings{Alexey:2012,
  Title                    = {Show No Weakness: Sequentially Consistent Specifications of {TSO}
 Libraries},
  Author                   = {Alexey Gotsman and
 Madanlal Musuvathi and
 Hongseok Yang},
  Booktitle                = {Distributed Computing - 26th International Symposium, {DISC} 2012,
 Salvador, Brazil, October 16-18, 2012. Proceedings},
  Year                     = {2012},
  Pages                    = {31--45},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/wdag/GotsmanMY12},
  Crossref                 = {DBLP:conf/wdag/2012},
  Doi                      = {10.1007/978-3-642-33651-5_3},
  Timestamp                = {Mon, 15 Oct 2012 15:25:23 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-33651-5_3}
}

@InProceedings{Henzinger:2013,
  Title                    = {Quantitative relaxation of concurrent data structures},
  Author                   = {Thomas A. Henzinger and
 Christoph M. Kirsch and
 Hannes Payer and
 Ali Sezgin and
 Ana Sokolova},
  Booktitle                = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
 Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25,
 2013},
  Year                     = {2013},
  Pages                    = {317--328},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/popl/HenzingerKPSS13},
  Crossref                 = {DBLP:conf/popl/2013},
  Doi                      = {10.1145/2429069.2429109},
  Timestamp                = {Fri, 18 Jan 2013 17:57:12 +0100},
  Url                      = {http://doi.acm.org/10.1145/2429069.2429109}
}

@InProceedings{Jagadeesan:2014,
  Title                    = {Between Linearizability and Quiescent Consistency - Quantitative Quiescent
 Consistency},
  Author                   = {Radha Jagadeesan and
 James Riely},
  Booktitle                = {Automata, Languages, and Programming - 41st International Colloquium,
 {ICALP} 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part
 {II}},
  Year                     = {2014},
  Pages                    = {220--231},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/icalp/JagadeesanR14},
  Crossref                 = {DBLP:conf/icalp/2014-2},
  Doi                      = {10.1007/978-3-662-43951-7_19},
  Timestamp                = {Fri, 13 Jun 2014 13:58:15 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-662-43951-7_19}
}

@InProceedings{Feng:2013,
  Title                    = {Modular verification of linearizability with non-fixed linearization
 points},
  Author                   = {Hongjin Liang and
 Xinyu Feng},
  Booktitle                = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
 {PLDI} '13, Seattle, WA, USA, June 16-19, 2013},
  Year                     = {2013},
  Pages                    = {459--470},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/pldi/LiangF13},
  Crossref                 = {DBLP:conf/pldi/2013},
  Doi                      = {10.1145/2462156.2462189},
  Timestamp                = {Sun, 09 Jun 2013 12:32:52 +0200},
  Url                      = {http://doi.acm.org/10.1145/2462156.2462189}
}

@InProceedings{Owens:2010,
  Title                    = {Reasoning about the Implementation of Concurrency Abstractions on
 x86-TSO},
  Author                   = {Scott Owens},
  Booktitle                = {{ECOOP} 2010 - Object-Oriented Programming, 24th European Conference,
 Maribor, Slovenia, June 21-25, 2010. Proceedings},
  Year                     = {2010},
  Pages                    = {478--503},
  Series                   = {Lecture Notes in Computer Science},
  Volume                   = {6183},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/Owens10},
  Crossref                 = {DBLP:conf/ecoop/2010},
  Doi                      = {10.1007/978-3-642-14107-2_23},
  Timestamp                = {Fri, 19 Sep 2014 08:37:40 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-14107-2_23}
}

@InProceedings{Owens:2009,
  Title                    = {A Better x86 Memory Model: x86-TSO},
  Author                   = {Scott Owens and
 Susmit Sarkar and
 Peter Sewell},
  Booktitle                = {TPHOLs},
  Year                     = {2009},
  Pages                    = {391-407},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/tphol/2009},
  Ee                       = {http://dx.doi.org/10.1007/978-3-642-03359-9_27}
}

@InProceedings{Schnoebelen:2001,
  Title                    = {Bisimulation and Other Undecidable Equivalences for Lossy
 Channel Systems},
  Author                   = {Ph. Schnoebelen},
  Booktitle                = {TACS},
  Year                     = {2001},
  Pages                    = {385-399},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Crossref                 = {DBLP:conf/tacs/2001},
  Ee                       = {http://dx.doi.org/10.1007/3-540-45500-0_19}
}

@InProceedings{Viktor:2009,
  Title                    = {Shape-Value Abstraction for Verifying Linearizability},
  Author                   = {Viktor Vafeiadis},
  Booktitle                = {Verification, Model Checking, and Abstract Interpretation, 10th International
 Conference, {VMCAI} 2009, Savannah, GA, USA, January 18-20, 2009.
 Proceedings},
  Year                     = {2009},
  Pages                    = {335--348},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/vmcai/Vafeiadis09},
  Crossref                 = {DBLP:conf/vmcai/2009},
  Doi                      = {10.1007/978-3-540-93900-9_27},
  Timestamp                = {Thu, 18 Dec 2008 20:07:01 +0100},
  Url                      = {http://dx.doi.org/10.1007/978-3-540-93900-9_27}
}

@InProceedings{Wimmer:2014,
  Title                    = {Data structures for task-based priority scheduling},
  Author                   = {Martin Wimmer and
 Francesco Versaci and
 Jesper Larsson Tr{\"{a}}ff and
 Daniel Cederman and
 Philippas Tsigas},
  Booktitle                = {{ACM} {SIGPLAN} Symposium on Principles and Practice of Parallel Programming,
 PPoPP '14, Orlando, FL, USA, February 15-19, 2014},
  Year                     = {2014},
  Pages                    = {379--380},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/ppopp/0003VTCT14},
  Crossref                 = {DBLP:conf/ppopp/2014},
  Doi                      = {10.1145/2555243.2555278},
  Timestamp                = {Sun, 09 Feb 2014 12:47:13 +0100},
  Url                      = {http://doi.acm.org/10.1145/2555243.2555278}
}

@InProceedings{Arijit:2013,
  Title                    = {Round-up: Runtime checking quasi linearizability of concurrent data
 structures},
  Author                   = {Lu Zhang and
 Arijit Chattopadhyay and
 Chao Wang},
  Booktitle                = {2013 28th {IEEE/ACM} International Conference on Automated Software
 Engineering, {ASE} 2013, Silicon Valley, CA, USA, November 11-15,
 2013},
  Year                     = {2013},
  Pages                    = {4--14},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/kbse/ZhangCW13},
  Crossref                 = {DBLP:conf/kbse/2013},
  Doi                      = {10.1109/ASE.2013.6693061},
  Timestamp                = {Mon, 21 Jul 2014 07:41:41 +0200},
  Url                      = {http://dx.doi.org/10.1109/ASE.2013.6693061}
}

@InProceedings{Cerny:2010,
  Title                    = {Model Checking of Linearizability of Concurrent List Implementations},
  Author                   = {\v{C}ern\'{y}, Pavol and Radhakrishna, Arjun and Zufferey, Damien and Chaudhuri, Swarat and Alur, Rajeev},
  Booktitle                = {Proceedings of the 22Nd International Conference on Computer Aided Verification},
  Year                     = {2010},

  Address                  = {Berlin, Heidelberg},
  Pages                    = {465--479},
  Publisher                = {Springer-Verlag},
  Series                   = {CAV'10},

  Acmid                    = {2144362},
  Doi                      = {10.1007/978-3-642-14295-6_41},
  ISBN                     = {3-642-14294-X, 978-3-642-14294-9},
  Location                 = {Edinburgh, UK},
  Numpages                 = {15},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-14295-6_41}
}

@Article{Parosh:2000,
  Title                    = {Algorithmic Analysis of Programs with Well Quasi-ordered
 Domains},
  Author                   = {Parosh Aziz Abdulla and
 Karlis Cerans and
 Bengt Jonsson and
 Yih-Kuen Tsay},
  Journal                  = {Inf. Comput.},
  Year                     = {2000},
  Number                   = {1-2},
  Pages                    = {109-127},
  Volume                   = {160},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Ee                       = {http://dx.doi.org/10.1006/inco.1999.2843}
}

@Article{Sarita:1996,
  Title                    = {Shared Memory Consistency Models: A Tutorial},
  Author                   = {Sarita V. Adve and
 Kourosh Gharachorloo},
  Journal                  = {IEEE Computer},
  Year                     = {1996},
  Number                   = {12},
  Pages                    = {66-76},
  Volume                   = {29},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Ee                       = {http://doi.ieeecomputersociety.org/10.1109/2.546611}
}

@InProceedings{Alur:1996,
  Title                    = {Model-checking of Correctness Conditions for Concurrent Objects},
  Author                   = {Alur, Rajeev and McMillan, Ken and Peled, Doron},
  Booktitle                = {Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science},
  Year                     = {1996},

  Address                  = {Washington, DC, USA},
  Pages                    = {219--},
  Publisher                = {IEEE Computer Society},
  Series                   = {LICS '96},

  Acmid                    = {788833},
  ISBN                     = {0-8186-7463-6},
  Url                      = {http://dl.acm.org/citation.cfm?id=788018.788833}
}

@Article{Shavit:1994,
  Title                    = {Counting Networks},
  Author                   = {James Aspnes and
 Maurice Herlihy and
 Nir Shavit},
  Journal                  = {J. {ACM}},
  Year                     = {1994},
  Number                   = {5},
  Pages                    = {1020--1048},
  Volume                   = {41},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/journals/jacm/AspnesHS94},
  Doi                      = {10.1145/185675.185815},
  Timestamp                = {Thu, 20 Nov 2003 12:28:00 +0100},
  Url                      = {http://doi.acm.org/10.1145/185675.185815}
}

@InProceedings{Atig:2010,
  Title                    = {On the Verification Problem for Weak Memory Models},
  Author                   = {Atig, Mohamed Faouzi and Bouajjani, Ahmed and Burckhardt, Sebastian and Musuvathi, Madanlal},
  Booktitle                = {Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  Year                     = {2010},

  Address                  = {New York, NY, USA},
  Pages                    = {7--18},
  Publisher                = {ACM},
  Series                   = {POPL '10},

  Acmid                    = {1706303},
  Doi                      = {10.1145/1706299.1706303},
  ISBN                     = {978-1-60558-479-9},
  Keywords                 = {infinite state systems, lossy channel systems, program verification, relaxed memory models},
  Location                 = {Madrid, Spain},
  Numpages                 = {12},
  Url                      = {http://doi.acm.org/10.1145/1706299.1706303}
}

@InProceedings{Batty:2011,
  Title                    = {Mathematizing C++ Concurrency},
  Author                   = {Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark},
  Booktitle                = {Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  Year                     = {2011},

  Address                  = {New York, NY, USA},
  Pages                    = {55--66},
  Publisher                = {ACM},
  Series                   = {POPL '11},

  Acmid                    = {1926394},
  Doi                      = {10.1145/1926385.1926394},
  ISBN                     = {978-1-4503-0490-0},
  Keywords                 = {relaxed memory models, semantics},
  Location                 = {Austin, Texas, USA},
  Numpages                 = {12},
  Url                      = {http://doi.acm.org/10.1145/1926385.1926394}
}

@InProceedings{Ahmed:2013,
  Title                    = {Checking and Enforcing Robustness against TSO},
  Author                   = {Ahmed Bouajjani and
 Egor Derevenetc and
 Roland Meyer},
  Booktitle                = {ESOP},
  Year                     = {2013},
  Pages                    = {533-553},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Ee                       = {http://dx.doi.org/10.1007/978-3-642-37036-6_29}
}

@InProceedings{Bouajjani:2013,
  Title                    = {Verifying Concurrent Programs Against Sequential Specifications},
  Author                   = {Bouajjani, Ahmed and Emmi, Michael and Enea, Constantin and Hamza, Jad},
  Booktitle                = {Proceedings of the 22Nd European Conference on Programming Languages and Systems},
  Year                     = {2013},

  Address                  = {Berlin, Heidelberg},
  Pages                    = {290--309},
  Publisher                = {Springer-Verlag},
  Series                   = {ESOP'13},

  Acmid                    = {2450291},
  Doi                      = {10.1007/978-3-642-37036-6_17},
  ISBN                     = {978-3-642-37035-9},
  Location                 = {Rome, Italy},
  Numpages                 = {20},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-37036-6_17}
}

@InProceedings{Sebastian:2008,
  Title                    = {Effective Program Verification for Relaxed Memory Models},
  Author                   = {Sebastian Burckhardt and
 Madanlal Musuvathi},
  Booktitle                = {CAV},
  Year                     = {2008},
  Pages                    = {107-120},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Ee                       = {http://dx.doi.org/10.1007/978-3-540-70545-1_12}
}

@Article{Robert:2005,
  Title                    = {Verifying Concurrent Data Structures by Simulation},
  Author                   = {Robert Colvin and
 Simon Doherty and
 Lindsay Groves},
  Journal                  = {Electr. Notes Theor. Comput. Sci.},
  Year                     = {2005},
  Number                   = {2},
  Pages                    = {93--110},
  Volume                   = {137},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/journals/entcs/ColvinDG05},
  Doi                      = {10.1016/j.entcs.2005.04.026},
  Timestamp                = {Mon, 19 Dec 2005 13:33:29 +0100},
  Url                      = {http://dx.doi.org/10.1016/j.entcs.2005.04.026}
}

@Article{Alain:2001,
  Title                    = {Well-structured transition systems everywhere!},
  Author                   = {Alain Finkel and
 Ph. Schnoebelen},
  Journal                  = {Theor. Comput. Sci.},
  Year                     = {2001},
  Number                   = {1-2},
  Pages                    = {63-92},
  Volume                   = {256},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Ee                       = {http://dx.doi.org/10.1016/S0304-3975(00)00102-X}
}

@InProceedings{Higman:1952,
  Title                    = {Ordering by divisibility in abstract algebras},
  Author                   = {Higman G},
  Booktitle                = {Proc. London Math. Soc.2},
  Year                     = {1952},
  Pages                    = {326-336}
}

@Book{Herilihy:2008,
  Title                    = {The Art of Multiprocessor Programming},
  Author                   = {Maurice Herlihy and 
 Nir Shavit},
  Year                     = {2008}
}

@Article{Herlihy:1990,
  Title                    = {Linearizability: A Correctness Condition for Concurrent Objects},
  Author                   = {Herlihy, Maurice P. and Wing, Jeannette M.},
  Journal                  = {ACM Trans. Program. Lang. Syst.},
  Year                     = {1990},

  Month                    = jul,
  Number                   = {3},
  Pages                    = {463--492},
  Volume                   = {12},

  Acmid                    = {78972},
  Address                  = {New York, NY, USA},
  Doi                      = {10.1145/78969.78972},
  ISSN                     = {0164-0925},
  Issue_date               = {July 1990},
  Numpages                 = {30},
  Publisher                = {ACM},
  Url                      = {http://doi.acm.org/10.1145/78969.78972}
}

@Book{Hoare:1985,
  Title                    = {Communicating Sequential Processes},
  Author                   = {C. A. R. Hoare},
  Publisher                = {Prentice-Hall},
  Year                     = {1985},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/books/ph/Hoare85},
  ISBN                     = {0-13-153271-5},
  Timestamp                = {Thu, 03 Jan 2002 11:51:40 +0100}
}

@Article{Lamport:1979,
  Title                    = {How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Progranm},
  Author                   = {L. Lamport},
  Journal                  = {IEEE Transactions on Computers},
  Year                     = {1979},
  Number                   = {9},
  Pages                    = {690-691},
  Volume                   = {28},

  Address                  = {Los Alamitos, CA, USA},
  Doi                      = {http://doi.ieeecomputersociety.org/10.1109/TC.1979.1675439},
  ISSN                     = {0018-9340},
  Publisher                = {IEEE Computer Society}
}

@InProceedings{Yang:2013,
  Title                    = {Verifying Linearizability via Optimized Refinement Checking},
  Author                   = {Yang Liu and
 Wei Chen and
 Yanhong A. Liu and
 Jun Sun and
 Shao Jie Zhang and
 Jin Song Dong},
  Year                     = {2013},
  Number                   = {7},
  Pages                    = {1018-1039},
  Volume                   = {39},

  Bibsource                = {DBLP, http://dblp.uni-trier.de},
  Ee                       = {http://doi.ieeecomputersociety.org/10.1109/TSE.2012.82},
  Journal                  = {IEEE Trans. Software Eng.}
}

@InProceedings{Manson:2005,
  Title                    = {The Java Memory Model},
  Author                   = {Manson, Jeremy and Pugh, William and Adve, Sarita V.},
  Booktitle                = {Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  Year                     = {2005},

  Address                  = {New York, NY, USA},
  Pages                    = {378--391},
  Publisher                = {ACM},
  Series                   = {POPL '05},

  Acmid                    = {1040336},
  Doi                      = {10.1145/1040305.1040336},
  ISBN                     = {1-58113-830-X},
  Keywords                 = {Java, concurrency, memory model, multithreading},
  Location                 = {Long Beach, California, USA},
  Numpages                 = {14},
  Url                      = {http://doi.acm.org/10.1145/1040305.1040336}
}

@InProceedings{Sarkar:2011,
  Title                    = {Understanding POWER Multiprocessors},
  Author                   = {Sarkar, Susmit and Sewell, Peter and Alglave, Jade and Maranget, Luc and Williams, Derek},
  Booktitle                = {Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation},
  Year                     = {2011},

  Address                  = {New York, NY, USA},
  Pages                    = {175--186},
  Publisher                = {ACM},
  Series                   = {PLDI '11},

  Acmid                    = {1993520},
  Doi                      = {10.1145/1993498.1993520},
  ISBN                     = {978-1-4503-0663-8},
  Keywords                 = {relaxed memory models, semantics},
  Location                 = {San Jose, California, USA},
  Numpages                 = {12},
  Url                      = {http://doi.acm.org/10.1145/1993498.1993520}
}

@Article{Schnoebelen:2002,
  Title                    = {Verifying lossy channel systems has nonprimitive recursive complexity},
  Author                   = {Philippe Schnoebelen},
  Journal                  = {Inf. Process. Lett.},
  Year                     = {2002},
  Number                   = {5},
  Pages                    = {251--261},
  Volume                   = {83},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/journals/ipl/Schnoebelen02},
  Doi                      = {10.1016/S0020-0190(01)00337-4},
  Timestamp                = {Tue, 12 May 2015 17:12:01 +0200},
  Url                      = {http://dx.doi.org/10.1016/S0020-0190(01)00337-4}
}

@Book{Smith:2000,
  Title                    = {The Object-Z Specification Language},
  Author                   = {Graeme Smith},
  Year                     = {2000}
}

@InProceedings{Vafeiadis:2010,
  Title                    = {Automatically Proving Linearizability},
  Author                   = {Vafeiadis, Viktor},
  Booktitle                = {Proceedings of the 22Nd International Conference on Computer Aided Verification},
  Year                     = {2010},

  Address                  = {Berlin, Heidelberg},
  Pages                    = {450--464},
  Publisher                = {Springer-Verlag},
  Series                   = {CAV'10},

  Acmid                    = {2144361},
  Doi                      = {10.1007/978-3-642-14295-6_40},
  ISBN                     = {3-642-14294-X, 978-3-642-14294-9},
  Location                 = {Edinburgh, UK},
  Numpages                 = {15},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-14295-6_40}
}

@TechReport{Vafeiadis:2007,
  Title                    = {{Modular fine-grained concurrency verification}},
  Author                   = {Vafeiadis, Viktor},
  Institution              = {University of Cambridge, Computer Laboratory},
  Year                     = {2008},
  Month                    = jul,
  Number                   = {UCAM-CL-TR-726},

  Url                      = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf}
}

@InProceedings{Martin:2009,
  Title                    = {Experience with Model Checking Linearizability},
  Author                   = {Martin T. Vechev and
 Eran Yahav and
 Greta Yorsh},
  Booktitle                = {Model Checking Software, 16th International {SPIN} Workshop, Grenoble,
 France, June 26-28, 2009. Proceedings},
  Year                     = {2009},
  Pages                    = {261--278},
  Publisher                = {Springer},
  Series                   = {Lecture Notes in Computer Science},
  Volume                   = {5578},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/conf/spin/VechevYY09},
  Doi                      = {10.1007/978-3-642-02652-2_21},
  Timestamp                = {Thu, 02 Jul 2009 22:03:53 +0200},
  Url                      = {http://dx.doi.org/10.1007/978-3-642-02652-2_21}
}

@InProceedings{Wang:2015,
  Title                    = {TSO-to-TSO linearizability is undecidable},
  Author                   = {Chao Wang and
 Yi Lv and
 Peng Wu},
  Booktitle                = {Automated Technology for Verification and Analysis - 13th International
 Symposium, {ATVA} 2015,
 Proceedings},
  Year                     = {2015},
  Pages                    = {264--280},

  Timestamp                = {Mon, 03 Nov 2014 14:32:36 +0100}
}

@TechReport{Wang:2015a,
  Title                    = {Bounded TSO-to-SC Linearizability is Decidable},
  Author                   = {Chao Wang and Yi Lv and Peng Wu},
  Institution              = {State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences},
  Year                     = {2015},
  Number                   = {ISCAS-SKLCS-15-11},

  Timestamp                = {2015.06.15}
}

@Book{David:1994,
  Title                    = {The SPARC Architecture Manual, Version 9},
  Author                   = {David L. Weaver and 
 Tom Germond},
  Year                     = {1994}
}