{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,31]],"date-time":"2026-08-31T04:14:12Z","timestamp":1788149652277,"version":"build-2803163510"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T00:00:00Z","timestamp":1771891200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T00:00:00Z","timestamp":1771891200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P36623"],"award-info":[{"award-number":["P36623"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100018706","name":"HORIZON EUROPE Widening participation and spreading excellence","doi-asserted-by":"publisher","award":["101160022"],"award-info":[{"award-number":["101160022"]}],"id":[{"id":"10.13039\/100018706","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ERC CoG ARTIST 101002685"],"award-info":[{"award-number":["ERC CoG ARTIST 101002685"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Netidee"},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["10.47379\/VRG11005"],"award-info":[{"award-number":["10.47379\/VRG11005"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2026,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The already challenging task of identifying the cause of a bug becomes even more cumbersome if those bugs disappear or change their behavior under observation. Such bugs occur in a range of contexts including elusive concurrency bugs as well as unintended system alterations during debugging and\u2014as a pun on the name of Werner Heisenberg\u2014are often referred to as Heisenbugs. Heisenbugs can be caused by various sources of nondeterminism on different system levels, many of which developers and testers might not even be aware of. This paper provides formal foundations for rigorously reasoning about causes of Heisenbugs. It provides a formal definition of Heisenbugs in terms of a hyperproperty and introduces a framework for determining the causality of Heisenbugs in presence of multiple candidate causes based on said hyperproperty. We analyze the properties of causes and the implications on practical causal analyses. We provide two small case studies and a taxonomy of potential causes of Heisenbugs.<\/jats:p>","DOI":"10.1007\/s10270-025-01345-7","type":"journal-article","created":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T04:24:14Z","timestamp":1771907054000},"page":"1059-1081","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A formalization of Heisenbugs and their causes in terms of hyperproperties"],"prefix":"10.1007","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6828-659X","authenticated-orcid":false,"given":"Sarah","family":"Sallinger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0143-632X","authenticated-orcid":false,"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,2,24]]},"reference":[{"key":"1345_CR1","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: Logic in Computer Science (LICS) (1988)"},{"issue":"2","key":"1345_CR2","first-page":"178","volume":"41","author":"J Alglave","year":"2012","unstructured":"Alglave, J.: A formal hierarchy of weak memory models. FMSD 41(2), 178\u2013210 (2012)","journal-title":"FMSD"},{"key":"1345_CR3","unstructured":"Baier, C., Dubslaff, C., Funke, F., Jantsch, S., Majumdar, R., Piribauer, J., Ziemek, R.: From verification to causality-based explications. In: ICALP (2021)"},{"key":"1345_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Formal Methods (FM). LNCS, vol.\u00a06664, pp. 200\u2013214. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"1345_CR5","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Computer Aided Verification (CAV) (2009)","DOI":"10.1007\/978-3-642-02658-4_11"},{"issue":"6","key":"1345_CR6","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1109\/90.811445","volume":"7","author":"JCR Bennett","year":"1999","unstructured":"Bennett, J.C.R., Partridge, C., Shectman, N.: Packet reordering is not pathological network behavior. IEEE\/ACM Trans. Netw. 7(6), 789\u2013798 (1999)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"1345_CR7","doi-asserted-by":"crossref","unstructured":"Beutner, R., Finkbeiner, B.: Autohyper: explicit-state model checking for hyperltl. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 13993, pp. 145\u2013163. Springer (2023)","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"1345_CR8","doi-asserted-by":"crossref","unstructured":"Brechelmacher, O., Nickovic, D., Nie\u00dfen, T., Sallinger, S., Weissenbacher, G.: Differential property monitoring for backdoor detection. In: Formal Engineering Methods (ICFEM). LNCS, vol. 15394, pp. 216\u2013236. Springer (2024)","DOI":"10.1007\/978-981-96-0617-7_13"},{"key":"1345_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: Nusmv 2: an opensource tool for symbolic model checking. In: Computer Aided Verification (CAV) (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"1345_CR10","unstructured":"Cimatti, A., Pecheur, C., Cavada, R.: Formal verification of diagnosability via symbolic model checking. In: International Joint Conference on Artificial Intelligence (IJCAI) (2003)"},{"issue":"6","key":"1345_CR11","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"1345_CR12","doi-asserted-by":"crossref","unstructured":"Coenen, N., Dachselt, R., Finkbeiner, B., Frenkel, H., Hahn, C., Horak, T., Metzger, N., Siber, J.: Explaining hyperproperty violations. In: Computer Aided Verification (CAV) (2022)","DOI":"10.1007\/978-3-031-13185-1_20"},{"key":"1345_CR13","doi-asserted-by":"crossref","unstructured":"Cotroneo, D., Grottke, M., Natella, R., Pietrantuono, R., Trivedi, K.S.: Fault triggers in open-source software: An experience report. In: International Symposium on Software Reliability Engineering (ISSRE) (2013)","DOI":"10.1109\/ISSRE.2013.6698917"},{"key":"1345_CR14","doi-asserted-by":"crossref","unstructured":"Dubslaff, C., Weis, K., Baier, C., Apel, S.: Causality in configurable software systems. In: International Conference on Software Engineering (ICSE) (2022)","DOI":"10.1145\/3510003.3510200"},{"key":"1345_CR15","doi-asserted-by":"crossref","unstructured":"Eck, M., Palomba, F., Castelluccio, M., Bacchelli, A.: Understanding flaky tests: the developer\u2019s perspective. In: Foundations of Software Engineering (ESEC\/FSE) (2019)","DOI":"10.1145\/3338906.3338945"},{"issue":"1","key":"1345_CR16","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S0004-3702(02)00271-0","volume":"142","author":"T Eiter","year":"2002","unstructured":"Eiter, T., Lukasiewicz, T.: Complexity results for structure-based causality. Artif. Intell. 142(1), 53\u201389 (2002)","journal-title":"Artif. Intell."},{"key":"1345_CR17","doi-asserted-by":"crossref","unstructured":"Erfani\u00a0Joorabchi, M., Mirzaaghaei, M., Mesbah, A.: Works for me! Characterizing non-reproducible bug reports. In: Mining Software Repositories (MSR) (2014)","DOI":"10.1145\/2597073.2597098"},{"key":"1345_CR18","doi-asserted-by":"publisher","unstructured":"Fellner, A.: Strong model-based mutation testing. Ph.D. thesis, TU Wien (2021). https:\/\/doi.org\/10.34726\/hss.2021.88481","DOI":"10.34726\/hss.2021.88481"},{"issue":"2","key":"1345_CR19","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/s10270-020-00850-1","volume":"20","author":"A Fellner","year":"2021","unstructured":"Fellner, A., Befrouei, M.T., Weissenbacher, G.: Mutation testing with hyperproperties. Softw. Syst. Model. 20(2), 405\u2013427 (2021). https:\/\/doi.org\/10.1007\/s10270-020-00850-1","journal-title":"Softw. Syst. Model."},{"key":"1345_CR20","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: Computer Aided Verification (CAV) (2015)","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"1345_CR21","doi-asserted-by":"crossref","unstructured":"Flur, S., Gray, K.E., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., Sewell, P.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Principles of Programming Languages (POPL) (2016)","DOI":"10.1145\/2837614.2837615"},{"issue":"1\u20132","key":"1345_CR22","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/S0004-3702(97)00047-7","volume":"97","author":"D Galles","year":"1997","unstructured":"Galles, D., Pearl, J.: Axioms of causal relevance. Artif. Intell. 97(1\u20132), 9\u201343 (1997)","journal-title":"Artif. Intell."},{"key":"1345_CR23","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1016\/j.tcs.2020.06.010","volume":"837","author":"G G\u00f6ssler","year":"2020","unstructured":"G\u00f6ssler, G., Stefani, J.B.: Causality analysis and fault ascription in component-based systems. Theor. Comput. Sci. 837, 158\u2013180 (2020)","journal-title":"Theor. Comput. Sci."},{"key":"1345_CR24","unstructured":"Gray, J.: Why do computers stop and what can be done about it? Tech. Rep. 85.7, PN87614, Tandem Computers (1986)"},{"key":"1345_CR25","unstructured":"Grottke, M., Trivedi, K.S.: A classification of software faults. In: International Symposium on Software Reliability Engineering (ISSRE) (2005)"},{"key":"1345_CR26","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: A modification of the Halpern-pearl definition of causality. In: International Joint Conference on Artificial Intelligence (IJCAI) (2015)","DOI":"10.7551\/mitpress\/9780262035026.003.0002"},{"key":"1345_CR27","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Pearl, J.: Causes and explanations: a structural-model approach: part 1: causes. Br. J. Philos. Sci. 56 (2005)","DOI":"10.1093\/bjps\/axi147"},{"key":"1345_CR28","unstructured":"ISO: IEC 9899:2018 Information technology-Programming languages-C (2018)"},{"key":"1345_CR29","unstructured":"Kollmansberger, S.: A truly random() heisenbug. https:\/\/www.kolls.net\/blog\/?p=222 (2017). Accessed: 2022-6-24"},{"key":"1345_CR30","volume-title":"Computer Networking: A Top-Down Approach","author":"JF Kurose","year":"2012","unstructured":"Kurose, J.F., Ross, K.W.: Computer Networking: A Top-Down Approach, 6th edn. Pearson, London (2012)","edition":"6"},{"key":"1345_CR31","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Foundations of Software Engineering (ESEC\/FSE) (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"1345_CR32","doi-asserted-by":"crossref","unstructured":"Lam, W., Godefroid, P., Nath, S., Santhiar, A., Thummalapenta, S.: Root causing flaky tests in a large-scale industrial setting. In: International Symposium on Software Testing and Analysis (ISSTA) (2019)","DOI":"10.1145\/3293882.3330570"},{"key":"1345_CR33","doi-asserted-by":"crossref","unstructured":"Leitner-Fischer, F., Leue, S.: Causality checking for complex system models. In: Verification, Model Checking and Abstract Interpretation (VMCAI) (2013)","DOI":"10.1007\/978-3-642-35873-9_16"},{"issue":"7","key":"1345_CR34","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N Leveson","year":"1993","unstructured":"Leveson, N., Turner, C.: An investigation of the Therac-25 accidents. IEEE Comput. 26(7), 18\u201341 (1993)","journal-title":"IEEE Comput."},{"issue":"17","key":"1345_CR35","doi-asserted-by":"publisher","first-page":"556","DOI":"10.2307\/2025310","volume":"70","author":"D Lewis","year":"1974","unstructured":"Lewis, D.: Causation. J. Philos. 70(17), 556\u2013567 (1974)","journal-title":"J. Philos."},{"key":"1345_CR36","volume-title":"Counterfactuals","author":"D Lewis","year":"2001","unstructured":"Lewis, D.: Counterfactuals. Wiley-Blackwell, Hoboken (2001)"},{"key":"1345_CR37","doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2008)","DOI":"10.1145\/1346281.1346323"},{"issue":"1","key":"1345_CR38","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MM.2007.5","volume":"27","author":"S Lu","year":"2007","unstructured":"Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: detecting atomicity violations via access-interleaving invariants. IEEE Micro 27(1), 26\u201335 (2007)","journal-title":"IEEE Micro"},{"issue":"3","key":"1345_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1353445.1353446","volume":"30","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D.: The pitfalls of verifying floating-point computations. Trans. Program. Lang. Syst. 30(3), 1\u201341 (2008)","journal-title":"Trans. Program. Lang. Syst."},{"key":"1345_CR40","first-page":"267","volume":"19","author":"J Moran","year":"2020","unstructured":"Moran, J., Augusto Alonso, C., Bertolino, A., de la Riva, C., Tuya, J.: Flakyloc: flakiness localization for reliable test suites in web applications. JWE 19, 267\u2013296 (2020)","journal-title":"JWE"},{"key":"1345_CR41","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing Heisenbugs in concurrent programs. In: Operating Systems Design and Implementation (OSDI) (2008)"},{"issue":"1","key":"1345_CR42","first-page":"1","volume":"31","author":"O Parry","year":"2021","unstructured":"Parry, O., Kapfhammer, G.M., Hilton, M., McMinn, P.: A survey of flaky tests. Trans. Softw. Eng. Methodol. 31(1), 1\u201374 (2021)","journal-title":"Trans. Softw. Eng. Methodol."},{"key":"1345_CR43","unstructured":"Patokallio, J.: Crashes only on Wednesdays. https:\/\/gyrovague.com\/2015\/07\/29\/crashes-only-on-wednesdays\/ (2015), accessed: 2022-6-23"},{"key":"1345_CR44","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: Programming Languages Design and Implementation (PLDI) (2004)","DOI":"10.1145\/996841.996845"},{"key":"1345_CR45","doi-asserted-by":"crossref","unstructured":"Rahman, M.M., Khomh, F., Castelluccio, M.: Why are some bugs non-reproducible? An empirical investigation using data fusion. In: International Conference on Software Maintenance and Evolution (ICSME) (2020)","DOI":"10.1109\/ICSME46990.2020.00063"},{"key":"1345_CR46","doi-asserted-by":"crossref","unstructured":"Ratliff, Z.B., Kuhn, D.R., Kacker, R.N., Lei, Y., Trivedi, K.S.: The relationship between software bug type and number of factors involved in failures. In: International Symposium on Software Reliability Engineering Workshops (ISSREW) (2016)","DOI":"10.1109\/ISSREW.2016.26"},{"key":"1345_CR47","unstructured":"Raymond, E.S.: The lost art of structure packing. http:\/\/www.catb.org\/esr\/structure-packing\/ (2020), accessed: 2022-6-24"},{"key":"1345_CR48","doi-asserted-by":"publisher","unstructured":"Sallinger, S., Weissenbacher, G., Zuleger, F.: A formalization of Heisenbugs and their causes. In: Software Engineering and Formal Methods (SEFM). Lecture Notes in Computer Science, vol 14323, pp. 282\u2013300. Springer Nature Switzerland, Cham. https:\/\/doi.org\/10.1007\/978-3-031-47115-5_16 (2023)","DOI":"10.1007\/978-3-031-47115-5_16"},{"key":"1345_CR49","unstructured":"Senftleben, M.: Operational characterization of weak memory consistency models. Master\u2019s thesis, University of Kaiserslautern (2013)"},{"key":"1345_CR50","volume-title":"Software Engineering","author":"I Sommerville","year":"2010","unstructured":"Sommerville, I.: Software Engineering, 9th edn. Addison-Wesley, New York (2010)","edition":"9"},{"key":"1345_CR51","volume-title":"Structured Computer Organization","author":"AS Tanenbaum","year":"2012","unstructured":"Tanenbaum, A.S., Austin, T.: Structured Computer Organization, 6th edn. Prentice Hall Press, Prentice (2012)","edition":"6"},{"key":"1345_CR52","unstructured":"Tarnovski, N.S.: Would you dare to change HashMap implementation? https:\/\/salnikov1.rssing.com\/browser.php?indx=17644734&item=22 (2013), accessed: 2022-6-24"},{"key":"1345_CR53","doi-asserted-by":"crossref","unstructured":"Terragni, V., Salza, P., Ferrucci, F.: A container-based infrastructure for fuzzy-driven root causing of flaky tests. In: International Conference on Software Engineering (ICSE) (2020)","DOI":"10.1145\/3377816.3381742"},{"issue":"1","key":"1345_CR54","first-page":"3","volume":"1","author":"M Thomas","year":"1994","unstructured":"Thomas, M.: The story of the therac-25 in lotos. High Integr. Syst. J. 1(1), 3\u201315 (1994)","journal-title":"High Integr. Syst. J."},{"key":"1345_CR55","doi-asserted-by":"crossref","unstructured":"Tretmans, J.: Test generation with inputs, outputs, and quiescence. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (1996)","DOI":"10.1007\/3-540-61042-1_42"},{"key":"1345_CR56","doi-asserted-by":"crossref","unstructured":"Zhou, G., Guo, B., Gao, X., Ning, W., Yan, Y.: Software analysis for transient faults: a review of recent methods. In: Advances in Intelligent Systems and Computing (AISC), vol.\u00a0298 (2014)","DOI":"10.1007\/978-3-319-07773-4_57"},{"key":"1345_CR57","doi-asserted-by":"crossref","unstructured":"Ziftci, C., Cavalcanti, D.: De-Flake your tests: automatically locating root causes of flaky tests in code at google. In: International Conference on Software Maintenance and Evolution (ICSME) (2020)","DOI":"10.1109\/ICSME46990.2020.00083"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01345-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-025-01345-7","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-025-01345-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,31]],"date-time":"2026-08-31T03:26:36Z","timestamp":1788146796000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-025-01345-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,24]]},"references-count":57,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2026,8]]}},"alternative-id":["1345"],"URL":"https:\/\/doi.org\/10.1007\/s10270-025-01345-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,2,24]]},"assertion":[{"value":"25 April 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 September 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 November 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2026","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}