references.bib

@article{Zave15,
  author = {Pamela Zave},
  title = {How to Make Chord Correct (Using a Stable Base)},
  journal = {CoRR},
  volume = {abs/1502.06461},
  year = {2015},
  url = {http://arxiv.org/abs/1502.06461},
  archivePrefix = {arXiv},
  eprint = {1502.06461},
  timestamp = {Wed, 07 Jun 2017 14:42:34 +0200},
  biburl = {http://dblp.org/rec/bib/journals/corr/Zave15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{stoica2001chord,
  title={Chord: A scalable peer to peer lookup service for internet applications},
  author={Stoica, Ion and Morris, Robert and Karger, David and Kaashoek, M Frans and Balakrishnan, Hari},
  journal={ACM SIGCOMM Computer Communication Review},
  volume={31},
  number={4},
  pages={149--160},
  year={2001},
  publisher={ACM}
}

@inproceedings{lamport2006checking,
  title={Checking a multithreaded algorithm with+ CAL},
  author={Lamport, Leslie},
  booktitle={DISC},
  volume={4167},
  pages={151--163},
  year={2006},
  organization={Springer}
}

@inproceedings{doherty2004dcas,
  title={DCAS is not a silver bullet for nonblocking algorithm design},
  author={Doherty, Simon and Detlefs, David L and Groves, Lindsay and Flood, Christine H and Luchangco, Victor and Martin, Paul A and Moir, Mark and Shavit, Nir and Steele Jr, Guy L},
  booktitle={Proceedings of the sixteenth annual ACM symposium on Parallelism in algorithms and architectures},
  pages={216--224},
  year={2004},
  organization={ACM}
}

@online{Pathfinder2013,
  author = {Rapitasystems},
  title = {What really happened to the software on the Mars Pathfinder spacecraft?},
  year = 2013,
  url = {https://www.rapitasystems.com/blog/what-really-happened-to-the-software-on-the-mars-pathfinder-spacecraft},
  note = "\url{https://www.rapitasystems.com/blog/what-really-happened-to-the-software-on-the-mars-pathfinder-spacecraft}",
}

@misc{wiki:therac,
  author = "Wikipedia contributors",
  title = "Therac-25 --- Wikipedia{,} The Free Encyclopedia",
  year = "2018",
  url = "\url{https://en.wikipedia.org/w/index.php?title=Therac-25&oldid=820552180}",
  note = "\url{https://en.wikipedia.org/w/index.php?title=Therac-25&oldid=820552180}",
}

@online{ms2017,
  author = {Microsoft},
  title = {A technical overview of Azure Cosmos DB},
  year = 2017,
  url = {https://azure.microsoft.com/en-us/blog/a-technical-overview-of-azure-cosmos-db/},
  note = "\url{https://azure.microsoft.com/en-us/blog/a-technical-overview-of-azure-cosmos-db/}",
}

@InProceedings{aws2014,
  author="Newcombe, Chris",
  editor="Ait Ameur, Yamine and Schewe, Klaus-Dieter",
  title="Why Amazon Chose TLA{\thinspace}+{\thinspace}          ",
  booktitle="Abstract State Machines, Alloy, B, TLA, VDM, and Z",
  year="2014",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="25--39",
  abstract="Since 2011, engineers at Amazon have been using TLA{\thinspace}+{\thinspace} to help solve difficult design problems in critical systems. This paper describes the reasons why we chose TLA{\thinspace}+{\thinspace} instead of other methods, and areas in which we would welcome further progress.",
  isbn="978-3-662-43652-3"
}


@online{elastic2017,
  author = {Elasticsearch},
  title = {Formal models of core Elasticsearch algorithms},
  year = 2017,
  url = {https://github.com/elastic/elasticsearch-formal-models},
  note = "\url{https://github.com/elastic/elasticsearch-formal-models}",
}

@online{mongo2016,
  author = {Siyuan Zhou},
  title = {TLA+ Spec of a simplified part of MongoDB replication system},
  year = 2017,
  url = {https://github.com/visualzhou/mongo-repl-tla},
  note = "\url{https://github.com/visualzhou/mongo-repl-tla}",
}

@online{hadoop2017,
  author = {Apache Hadoop},
  title = {Introduce Coordination Engine interface},
  year = 2017,
  url = {https://issues.apache.org/jira/browse/HADOOP-10641},
  note = "\url{https://issues.apache.org/jira/browse/HADOOP-10641}",
}

@online{jettify2016,
  author = {jettify},
  title = {aiorwlock implementation with bug},
  year = 2017,
  url = {https://github.com/aio-libs/aiorwlock/blob/v0.4.0/aiorwlock/__init__.py},
  note = "\url{https://github.com/aio-libs/aiorwlock/blob/v0.4.0/aiorwlock/__init__.py}",
}

@online{azurewebsites,
  author = {lamport},
  title = {The TLA Toolbox home page},
  year = 2018,
  url = {http://lamport.azurewebsites.net/tla/toolbox.html},
  note = "\url{http://lamport.azurewebsites.net/tla/toolbox.html}",
}

@online{principlesofchaos,
  author = {azurewebsites.org},
  title = {Principles of Chaos Engineering},
  year = 2018,
  url = {http://principlesofchaos.org},
  note = "\url{http://principlesofchaos.org}",
}


@online{mit2002,
  author = {mit.edu},
  title = {MIT 16.35 Aerospace Software Engineering},
  year = 2002,
  url = {http://web.mit.edu/16.35/www/lecturenotes/FormalMethods.pdf},
  note = "\url{http://web.mit.edu/16.35/www/lecturenotes/FormalMethods.pdf}",
}

@online{lkml2018,
  author = {lkml.org},
  title = {kernel/locking: qspinlock improvements},
  year = 2018,
  url = {https://lkml.org/lkml/2018/4/5/496},
  note = "\url{https://lkml.org/lkml/2018/4/5/496}",
}

@online{charpov2014,
  author = {charpov},
  title = {An Example of Debugging Java with a Model Checker},
  year = 2014,
  url = {http://www.cs.unh.edu/~charpov/teaching-cs745_845-example.html},
  note = "\url{http://www.cs.unh.edu/~charpov/teaching-cs745_845-example.html}",
}