Bila, Eleni, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. “Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.”https://doi.org/10.1007/978-3-030-50086-3‑3__In Formal Techniques for Distributed Objects, Components, and Systems - 40th IFIP WG 6.1 International Conference, FORTE 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, edited by Alexey Gotsman and Ana Sokolova, 12136:39–58. Lecture Notes in Computer Science. Springer, 2020.https://doi.org/10.1007/978-3-030-50086-3‑3 .

Derrick, John, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. “Verifying Correctness of Persistent Concurrent Data Structures.”https://doi.org/10.1007/978-3-030-30942-8‑12__In Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, 179–95, 2019.https://doi.org/10.1007/978-3-030-30942-8‑12 .

König, Jürgen, and Heike Wehrheim. “Data Independence for Software Transactional Memory.”https://doi.org/10.1007/978-3-030-20652-9‑18__In NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, edited by Julia M. Badger and Kristin Yvonne Rozier, 11460:263–79. Lecture Notes in Computer Science. Springer, 2019.https://doi.org/10.1007/978-3-030-20652-9‑18 .

Doherty, Simon, Brijesh Dongol, Heike Wehrheim, and John Derrick. “Verifyinghttps://doi.org/10.1145/3293883.3295702__Programs Operationally.”https://doi.org/10.1145/3293883.3295702__In Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2019, Washington, DC, USA, February 16-20, 2019, edited by Jeffrey K. Hollingsworth and Idit Keidar, 355–65. ACM, 2019.https://doi.org/10.1145/3293883.3295702 .

Schellhorn, Gerhard, Monika Wedel, Oleg Travkin, Jürgen König, and Heike Wehrheim. “FastLane Is Opaque – a Case Study in Mechanized Proofs of Opacity.”https://doi.org/10.1007/978-3-319-92970-5_7__In Software Engineering and Formal Methods, 105–20. Cham: Springer International Publishing, 2018.https://doi.org/10.1007/978-3-319-92970-5_7 .

König, Jürgen, and Heike Wehrheim. “Value-Based or Conflict-Based? Opacity Definitions for STMs.”https://doi.org/10.1007/978-3-319-67729-3_8__In Theoretical Aspects of Computing - ICTAC 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, edited by Dang Van Hung and Deepak Kapur, 118--135. Lecture Notes in Computer Science, 2017.https://doi.org/10.1007/978-3-319-67729-3_8 .

Doherty, Simon, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. “Proving Opacity of a Pessimistic STM.”https://doi.org/10.4230/LIPIcs.OPODIS.2016.35__In 20th International Conference on Principles of Distributed Systems, OPODIS 2016, December 13-16, 2016, Madrid, Spain, edited by Panagiota Fatourou, Ernesto Jim\rquote enez, and Fernando Pedone, 35:1--35:17. LIPIcs, 2016.https://doi.org/10.4230/LIPIcs.OPODIS.2016.35 .

Derrick, John, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, and Heike Wehrheim. “Verifying Opacity of a Transactional Mutex Lock.”https://doi.org/10.1007/978-3-319-19249-9_11__In FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, edited by Nikolaj Bjrner and Frank S. de Boer, 161--177. Lecture Notes in Computer Science, 2015.https://doi.org/10.1007/978-3-319-19249-9_11 .