@InProceedings{doherty_et_al:LIPIcs.OPODIS.2016.35, author = {Doherty, Simon and Dongol, Brijesh and Derrick, John and Schellhorn, Gerhard and Wehrheim, Heike}, title = {{Proving Opacity of a Pessimistic STM}}, booktitle = {20th International Conference on Principles of Distributed Systems (OPODIS 2016)}, pages = {35:1--35:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-031-6}, ISSN = {1868-8969}, year = {2017}, volume = {70}, editor = {Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.35}, URN = {urn:nbn:de:0030-drops-71040}, doi = {10.4230/LIPIcs.OPODIS.2016.35}, annote = {Keywords: Pessimistic STMs, Opacity, Verification, Isabelle, Simulation, TMS2} }