Doherty, Simon; Dalvandi, Sadegh; Dongol, Brijesh; Wehrheim, Heike Unifying operational weak memory verification: an axiomatic approach. (English) Zbl 1508.68216 ACM Trans. Comput. Log. 23, No. 4, Article No. 27, 39 p. (2022). MSC: 68Q60 68Q85 PDFBibTeX XMLCite \textit{S. Doherty} et al., ACM Trans. Comput. Log. 23, No. 4, Article No. 27, 39 p. (2022; Zbl 1508.68216) Full Text: DOI
Bila, Eleni; Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Wehrheim, Heike Modularising verification of durable opacity. (English) Zbl 07577571 Log. Methods Comput. Sci. 18, No. 3, Paper No. 7, 36 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{E. Bila} et al., Log. Methods Comput. Sci. 18, No. 3, Paper No. 7, 36 p. (2022; Zbl 07577571) Full Text: arXiv Link
König, Jürgen; Wehrheim, Heike On the correctness problem for serializability. (English) Zbl 07500637 Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2021. 18th international colloquium, virtual event, Nur-Sultan, Kazakhstan, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12819, 47-64 (2021). MSC: 68Qxx PDFBibTeX XMLCite \textit{J. König} and \textit{H. Wehrheim}, Lect. Notes Comput. Sci. 12819, 47--64 (2021; Zbl 07500637) Full Text: DOI
Bila, Eleni; Doherty, Simon; Dongol, Brijesh; Derrick, John; Schellhorn, Gerhard; Wehrheim, Heike Defining and verifying durable opacity: correctness for persistent software transactional memory. (English) Zbl 1511.68072 Gotsman, Alexey (ed.) et al., 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. Cham: Springer. Lect. Notes Comput. Sci. 12136, 39-58 (2020). MSC: 68N30 68N19 PDFBibTeX XMLCite \textit{E. Bila} et al., Lect. Notes Comput. Sci. 12136, 39--58 (2020; Zbl 1511.68072) Full Text: DOI arXiv
Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike Mechanized proofs of opacity: a comparison of two techniques. (English) Zbl 1395.68186 Formal Asp. Comput. 30, No. 5, 597-625 (2018). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{J. Derrick} et al., Formal Asp. Comput. 30, No. 5, 597--625 (2018; Zbl 1395.68186) Full Text: DOI
Derrick, John; Dongol, Brijesh; Schellhorn, Gerhard; Travkin, Oleg; Wehrheim, Heike Verifying opacity of a transactional mutex lock. (English) Zbl 1427.68190 Bjørner, Nikolaj (ed.) et al., FM 2015: formal methods. 20th international symposium, Oslo, Norway, June 24–26, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9109, 161-177 (2015). MSC: 68Q85 68Q60 PDFBibTeX XMLCite \textit{J. Derrick} et al., Lect. Notes Comput. Sci. 9109, 161--177 (2015; Zbl 1427.68190) Full Text: DOI Link
Schneider, Steve; Treharne, Helen; Wehrheim, Heike The behavioural semantics of Event-B refinement. (English) Zbl 1342.68211 Formal Asp. Comput. 26, No. 2, 251-280 (2014). MSC: 68Q60 68Q55 PDFBibTeX XMLCite \textit{S. Schneider} et al., Formal Asp. Comput. 26, No. 2, 251--280 (2014; Zbl 1342.68211) Full Text: DOI Link
Schellhorn, Gerhard; Derrick, John; Wehrheim, Heike A sound and complete proof technique for linearizability of concurrent data structures. (English) Zbl 1354.68066 ACM Trans. Comput. Log. 15, No. 4, Article No. 31, 37 p. (2014). MSC: 68P05 68Q60 68Q85 68T15 PDFBibTeX XMLCite \textit{G. Schellhorn} et al., ACM Trans. Comput. Log. 15, No. 4, Article No. 31, 37 p. (2014; Zbl 1354.68066) Full Text: DOI Link
Ruhroth, Thomas; Wehrheim, Heike Model evolution and refinement. (English) Zbl 1243.68156 Sci. Comput. Program. 77, No. 3, 270-289 (2012). MSC: 68N99 68Q60 PDFBibTeX XMLCite \textit{T. Ruhroth} and \textit{H. Wehrheim}, Sci. Comput. Program. 77, No. 3, 270--289 (2012; Zbl 1243.68156) Full Text: DOI
Derrick, John; Wehrheim, Heike Model transformations across views. (English) Zbl 1187.68161 Sci. Comput. Program. 75, No. 3, 192-210 (2010). MSC: 68N99 PDFBibTeX XMLCite \textit{J. Derrick} and \textit{H. Wehrheim}, Sci. Comput. Program. 75, No. 3, 192--210 (2010; Zbl 1187.68161) Full Text: DOI
Estler, H.-Christian; Wehrheim, Heike Alloy as a refactoring checker? (English) Zbl 1283.68205 Boiten, Eerke (ed.) et al., Proceedings of the 13th BCS-FACS refinement workshop (REFINE 2008), Turku, Finland, May 27, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 214, 331-357 (2008). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{H. C. Estler} and \textit{H. Wehrheim}, Electron. Notes Theor. Comput. Sci. 214, 331--357 (2008; Zbl 1283.68205) Full Text: DOI
Möller, Michael; Olderog, Ernst-Rüdiger; Rasch, Holger; Wehrheim, Heike Integrating a formal method into a software engineering process with UML and Java. (English) Zbl 1141.68024 Formal Asp. Comput. 20, No. 2, 161-204 (2008). MSC: 68N15 68Q60 PDFBibTeX XMLCite \textit{M. Möller} et al., Formal Asp. Comput. 20, No. 2, 161--204 (2008; Zbl 1141.68024) Full Text: DOI
Derrick, John; Wehrheim, Heike On using data abstractions for model checking refinements. (English) Zbl 1111.68077 Acta Inf. 44, No. 1, 41-71 (2007). MSC: 68Q60 PDFBibTeX XMLCite \textit{J. Derrick} and \textit{H. Wehrheim}, Acta Inf. 44, No. 1, 41--71 (2007; Zbl 1111.68077) Full Text: DOI