{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T09:18:20Z","timestamp":1765531100697,"version":"3.48.0"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T00:00:00Z","timestamp":1761523200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T00:00:00Z","timestamp":1761523200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"CISPA - Helmholtz-Zentrum f\u00fcr Informationssicherheit gGmbH"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Many important hyperliveness properties, such as refinement and generalized non-interference, fall into the class of\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\forall \\exists$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    hyperproperties, and require, for each execution trace of a system, the existence of another execution trace relating to the first one in a certain way. The alternation of quantifiers in the specification renders these hyperproperties extremely difficult to verify, or even just to test. Indeed, contrary to trace properties, where it suffices to find a single counterexample trace, refuting a\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\forall \\exists$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    hyperproperty requires not only to find a trace, but also a proof that no second trace exists that satisfies the specified relation with the first trace. As a consequence, automated testing of\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\forall \\exists$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    hyperproperties falls out of the scope of existing automated testing tools. In this paper, we present a fully automated approach to detect violations of\n                    <jats:inline-formula>\n                      <jats:tex-math>$$\\forall \\exists$$<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    hyperproperties in synchronous and asynchronous infinite-state systems. Our approach extends bug-finding techniques based on symbolic execution with support for trace quantification. We provide a prototype implementation of our approach, and demonstrate its effectiveness on a set of challenging examples.\n                  <\/jats:p>","DOI":"10.1007\/s00236-025-00504-z","type":"journal-article","created":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T04:46:27Z","timestamp":1761540387000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic execution for refuting \u2200\u2203\u00a0hyperproperties"],"prefix":"10.1007","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2307-2296","authenticated-orcid":false,"given":"Arthur","family":"Correnson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7712-0006","authenticated-orcid":false,"given":"Tobias","family":"Nie\u00dfen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0143-632X","authenticated-orcid":false,"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,27]]},"reference":[{"issue":"7","key":"504_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/390013.808479","volume":"5","author":"FE Allen","year":"1970","unstructured":"Allen, F.E.: Control flow analysis. ACM SIGPLAN Notices 5(7), 1\u201319 (1970). https:\/\/doi.org\/10.1145\/390013.808479","journal-title":"ACM SIGPLAN Notices"},{"key":"504_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press Ser, The MIT Press, Cambridge, Massachusetts and London, England (2008)"},{"key":"504_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C., Brain, M., et\u00a0al.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman D, Rosu G (eds) Tools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, Cham, pp 415\u2013442 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"504_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004. IEEE, Pacific Grove, CA, USA, pp 100\u2013114,(2004). https:\/\/doi.org\/10.1109\/CSFW.2004.1310735","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"504_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Crespo, JM., Kunz, C.: Relational Verification Using Product Programs. In: Butler M, Schulte W (eds) FM 2011: Formal Methods. Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, pp 200\u2013214 (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"504_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., D\u2019Argenio, PR., Finkbeiner, B., et\u00a0al.: Facets of software doping. In: Margaria T, Steffen B (eds) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. Springer International Publishing, Cham, pp 601\u2013608 (2016.) https:\/\/doi.org\/10.1007\/978-3-319-47169-3_46","DOI":"10.1007\/978-3-319-47169-3_46"},{"key":"504_CR7","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Henzinger, TA., Nickovic, D., et\u00a0al.: Hypernode Automata. LIPIcs, Volume 279, CONCUR 2023 279:21:1\u201321:16 (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.21","DOI":"10.4230\/LIPICS.CONCUR.2023.21"},{"key":"504_CR8","first-page":"5","volume-title":"Handook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics","author":"J Barwise","year":"1977","unstructured":"Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, vol. 90, pp. 5\u201346. Elsevier (1977)"},{"key":"504_CR9","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., et\u00a0al.: A Temporal Logic for Asynchronous Hyperproperties. In: Silva A, Leino KRM (eds) Computer Aided Verification. Springer International Publishing, Cham, pp 694\u2013717 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"504_CR10","doi-asserted-by":"publisher","unstructured":"Beutner, R.: Automated software verification of hyperliveness. In: Finkbeiner B, Kov\u00e1cs L (eds) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham, pp 196\u2013216 (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_10","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"504_CR11","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeine, B.: Prophecy Variables for Hyperproperty Verification. In: 2022 IEEE 35th Computer Security Foundations Symposium (CSF), pp 471\u2013485 (2022a). https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"504_CR12","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Software Verification of Hyperproperties Beyond k-Safety. In: Shoham S, Vizel Y (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 341\u2013362 (2022b). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_17","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"504_CR13","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: Explicit-State Model Checking for HyperLTL. In: Sankaranarayanan S, Sharygina N (eds) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Cham, Lecture Notes in Computer Science, pp 145\u2013163 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"504_CR14","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E., et\u00a0al.: Symbolic Model Checking without BDDs. In: Cleaveland WR (ed) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, pp 193\u2013207 (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"504_CR15","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., et al.: Bounded model checking. Adv Comput 58, 117\u2013148 (2003). https:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Bounded model checking. Adv Comput"},{"key":"504_CR16","doi-asserted-by":"publisher","unstructured":"de\u00a0Boer, FS., Bonsangue, M.: On the Nature of Symbolic Execution. In: ter Beek MH, McIver A, Oliveira JN (eds) Formal Methods \u2013 The Next 30 Years. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 64\u201380 (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_6","DOI":"10.1007\/978-3-030-30942-8_6"},{"key":"504_CR17","doi-asserted-by":"publisher","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Vauthier, C.: QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29, pp. 78\u201395. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_5","DOI":"10.1007\/978-3-031-38499-8_5"},{"key":"504_CR18","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., Sanchez, C., Schneider, G.: Monitoring Hyperproperties by Combining Static Analysis and Runtime Verification. In: Margaria T, Steffen B (eds) Leveraging Applications of Formal Methods, Verification and Validation. Verification. Springer International Publishing, Cham, pp 8\u201327 (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_2","DOI":"10.1007\/978-3-030-03421-4_2"},{"key":"504_CR19","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Peron, A., Sanchez, C.: Asynchronous Extensions of HyperLTL. In: 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). IEEE, Rome, Italy, pp 1\u201313 (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470583, https:\/\/ieeexplore.ieee.org\/document\/9470583\/","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"504_CR20","doi-asserted-by":"publisher","unstructured":"Bucur, S., Ureche, V., Zamfir, C., et\u00a0al.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the sixth conference on Computer systems. Association for Computing Machinery, New York, NY, USA, EuroSys \u201911, pp 183\u2013198 (2011). https:\/\/doi.org\/10.1145\/1966445.1966463","DOI":"10.1145\/1966445.1966463"},{"key":"504_CR21","doi-asserted-by":"publisher","unstructured":"Cadar, C., Ganesh, V., Pawlowski, PM., et\u00a0al.: EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on Computer and communications security. Association for Computing Machinery, New York, NY, USA, CCS \u201906, pp 322\u2013335 (2006). https:\/\/doi.org\/10.1145\/1180405.1180445","DOI":"10.1145\/1180405.1180445"},{"key":"504_CR22","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on Operating systems design and implementation. USENIX Association, USA, OSDI\u201908, pp 209\u2013224 (2008)"},{"issue":"8","key":"504_CR23","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/2240236.2240262","volume":"55","author":"S Chaudhuri","year":"2012","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM 55(8), 107\u2013115 (2012). https:\/\/doi.org\/10.1145\/2240236.2240262","journal-title":"Commun. ACM"},{"issue":"1","key":"504_CR24","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., et al.: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","journal-title":"Formal Methods in System Design"},{"issue":"6","key":"504_CR25","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). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"504_CR26","doi-asserted-by":"publisher","unstructured":"Clarkson, MR., Finkbeiner, B., Koleini, M., et\u00a0al.: Temporal Logics for Hyperproperties. In: Abadi M, Kremer S (eds) Principles of Security and Trust. Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, pp 265\u2013284, (2014) https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"504_CR27","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., et\u00a0al.: Verifying Hyperliveness. In: Dillig I, Tasiran S (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 121\u2013139 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"504_CR28","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hofmann, J., et\u00a0al.: Smart Contract Synthesis Modulo Hyperproperties. In: 2023 IEEE 36th Computer Security Foundations Symposium (CSF). IEEE, Dubrovnik, Croatia, pp 276\u2013291 (2023). https:\/\/doi.org\/10.1109\/CSF57540.2023.00006","DOI":"10.1109\/CSF57540.2023.00006"},{"key":"504_CR29","doi-asserted-by":"publisher","unstructured":"Correnson, A., Steinh\u00f6fel, D.: Engineering a formally verified automated bug finder. In: Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Association for Computing Machinery, New York, NY, USA, ESEC\/FSE 2023, pp 1165\u20131176 (2023). https:\/\/doi.org\/10.1145\/3611643.3616290","DOI":"10.1145\/3611643.3616290"},{"key":"504_CR30","doi-asserted-by":"publisher","unstructured":"Correnson, A., Nie\u00dfen, T., Finkbeiner, B., et\u00a0al.: Finding $$\\forall \\exists$$ Hyperbugs using Symbolic Execution. Proc ACM Program Lang 8(OOPSLA2):321:1420\u2013321:1445 (2024) https:\/\/doi.org\/10.1145\/3689761","DOI":"10.1145\/3689761"},{"key":"504_CR31","doi-asserted-by":"publisher","unstructured":"Daniel, LA., Bardin, S., Rezk, T.: Hunting the haunter - efficient relational symbolic execution for spectre with Haunted RelSE. Proceedings 2021 Network and Distributed System Security Symposium (2021). https:\/\/doi.org\/10.14722\/ndss.2021.24286","DOI":"10.14722\/ndss.2021.24286"},{"key":"504_CR32","doi-asserted-by":"publisher","DOI":"10.1145\/3563037","author":"LA Daniel","year":"2023","unstructured":"Daniel, L.A., Bardin, S., Rezk, T.: Binsec\/Rel: Symbolic binary analyzer for security with applications to constant-time and secret-erasure. ACM Trans Priv Secur (2023). https:\/\/doi.org\/10.1145\/3563037","journal-title":"ACM Trans Priv Secur"},{"issue":"PLDI","key":"504_CR33","doi-asserted-by":"publisher","DOI":"10.1145\/3656437","volume":"8","author":"T Dardinier","year":"2024","unstructured":"Dardinier, T., M\u00fcller, P.: Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. Proc ACM Program Lang 8(PLDI), 207:1485\u2013207:1509 (2024). https:\/\/doi.org\/10.1145\/3656437","journal-title":"Proc ACM Program Lang"},{"issue":"OOPSLA2","key":"504_CR34","doi-asserted-by":"publisher","first-page":"1279","DOI":"10.1145\/3689756","volume":"8","author":"T Dardinier","year":"2024","unstructured":"Dardinier, T., Li, A., M\u00fcller, P.: Hypra: A Deductive Program Verifier for Hyper Hoare Logic. Proceedings of the ACM on Programming Languages 8(OOPSLA2), 1279\u20131308 (2024). https:\/\/doi.org\/10.1145\/3689756","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"504_CR35","doi-asserted-by":"publisher","unstructured":"Dickerson, R., Ye, Q., Zhang, MK., et\u00a0al.: RHLE: Modular Deductive Verification of Relational $$\\forall \\exists$$ Properties. In: Sergey I (ed) Programming Languages and Systems. Springer, Cham, Lecture Notes in Computer Science, pp 67\u201387 (2022). https:\/\/doi.org\/10.1007\/978-3-031-21037-2_4","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"504_CR36","doi-asserted-by":"publisher","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., et\u00a0al.: Fairness Modulo Theory: A New Approach to LTL Software Model Checking. In: Kroening D, P\u0103s\u0103reanu CS (eds) Computer Aided Verification, vol 9206. Springer International Publishing, Cham, p 49\u201366 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_4","DOI":"10.1007\/978-3-319-21690-4_4"},{"key":"504_CR37","doi-asserted-by":"publisher","unstructured":"Doveri, K., Ganty, P., Mazzocchi, N.: FORQ-Based Language Inclusion Formal Testing. In: Shoham S, Vizel Y (eds) Computer Aided Verification. Springer International Publishing, Cham, pp 109\u2013129 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_6","DOI":"10.1007\/978-3-031-13188-2_6"},{"key":"504_CR38","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere A, Bloem R (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 737\u2013744 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"504_CR39","doi-asserted-by":"publisher","unstructured":"Farzan, A., Vandikas, A.: Automated Hypersafety Verification. In: Dillig I, Tasiran S (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 200\u2013218 (2019a). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"504_CR40","doi-asserted-by":"publisher","DOI":"10.1145\/3371081","author":"A Farzan","year":"2019","unstructured":"Farzan, A., Vandikas, A.: Reductions for safety proofs. Proc ACM Program Lang (2019b). https:\/\/doi.org\/10.1145\/3371081","journal-title":"Proc ACM Program Lang"},{"key":"504_CR41","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, MN., S\u00e1nchez, C.: Algorithms for Model Checking HyperLTL and HyperCTL$$^\\ast$$. In: Kroening D, P\u0103s\u0103reanu CS (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 30\u201348 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"504_CR42","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Frenkel, H., Hofmann, J.: Automata-Based Software Model Checking of Hyperproperties. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods, pp. 361\u2013379. Springer Nature Switzerland, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_22","DOI":"10.1007\/978-3-031-33170-1_22"},{"key":"504_CR43","doi-asserted-by":"crossref","unstructured":"Floyd, RW.: Assigning meanings to programs. In: Proceedings of Symposia in Applied Mathematics, vol\u00a019. Amer. Math. Soc., Providence, R.I., pp 19\u201332 (1967). https:\/\/mathscinet.ams.org\/mathscinet-getitem?mr=235771","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"504_CR44","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"JH Gallier","year":"2015","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving, 2nd edn. Dover Books On Computer Science, Dover Publications Inc, Mineola, New York (2015)","edition":"2"},{"key":"504_CR45","unstructured":"Godefroid, P.: The soundness of bugs is what matters (position statement). In: BUGS\u20192005 (PLDI\u20192005 Workshop on the Evaluation of Software Defect Detection Tools) (2005)"},{"issue":"6","key":"504_CR46","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1064978.1065036","volume":"40","author":"P Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. ACM SIGPLAN Notices 40(6), 213\u2013223 (2005). https:\/\/doi.org\/10.1145\/1064978.1065036","journal-title":"ACM SIGPLAN Notices"},{"key":"504_CR47","doi-asserted-by":"publisher","unstructured":"Hsu, TH., S\u00e1nchez, C., Bonakdarpour, B.: Bounded Model Checking for Hyperproperties. In: Groote JF, Larsen KG (eds) Tools and Algorithms for the Construction and Analysis of Systems, vol 12651. Springer International Publishing, Cham, p 94\u2013112 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"504_CR48","doi-asserted-by":"publisher","unstructured":"Hsu, TH., Bonakdarpour, B., Finkbeiner, B., et\u00a0al.: Bounded Model Checking for Asynchronous Hyperproperties. In: Sankaranarayanan S, Sharygina N (eds) Tools and Algorithms for the Construction and Analysis of Systems. Springer Nature Switzerland, Cham, pp 29\u201346 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_2","DOI":"10.1007\/978-3-031-30823-9_2"},{"key":"504_CR49","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Shoham, S., Vizel, Y.: Hyperproperty verification as CHC satisfiability. In: Weirich S (ed) Programming Languages and Systems. Springer, Cham, pp 212\u2013241 (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_9","DOI":"10.1007\/978-3-031-57267-8_9"},{"key":"504_CR50","doi-asserted-by":"publisher","unstructured":"Jhala, R., Podelski, A., Rybalchenko, A.: Predicate abstraction for program verification: Safety and termination. Handbook of Model Checking pp 447\u2013491 (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_15","DOI":"10.1007\/978-3-319-10575-8_15"},{"issue":"7","key":"504_CR51","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"issue":"11","key":"504_CR52","doi-asserted-by":"publisher","first-page":"2312","DOI":"10.1109\/TSE.2019.2946563","volume":"47","author":"VJ Manes","year":"2021","unstructured":"Manes, V.J., Han, H., Han, C., et al.: The Art, Science, and Engineering of Fuzzing: A Survey. IEEE Trans. Software Eng. 47(11), 2312\u20132331 (2021). https:\/\/doi.org\/10.1109\/TSE.2019.2946563","journal-title":"IEEE Trans. Software Eng."},{"key":"504_CR53","doi-asserted-by":"publisher","unstructured":"McCullough, D.:Noninterference and the composability of security properties. In: Proceedings. 1988 IEEE Symposium on Security and Privacy. IEEE Comput. Soc. Press, Oakland, CA, USA, pp 177\u2013186 (1988). https:\/\/doi.org\/10.1109\/SECPRI.1988.8110","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"504_CR54","doi-asserted-by":"publisher","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp 79\u201393 (1994). https:\/\/doi.org\/10.1109\/RISP.1994.296590","DOI":"10.1109\/RISP.1994.296590"},{"key":"504_CR55","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"504_CR56","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, AJ.: Viper: A Verification Infrastructure for Permission-Based Reasoning. In: Jobstmann B, Leino KRM (eds) Verification, Model Checking, and Abstract Interpretation. Springer, Berlin, Heidelberg, pp 41\u201362 (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"504_CR57","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting Enumerative Instantiation. In: Beyer D, Huisman M (eds) Tools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, Cham, pp 112\u2013131 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_7","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"504_CR58","doi-asserted-by":"publisher","unstructured":"Sabelfeld, A., Myers, AC.: A Model for Delimited Information Release. In: Futatsugi K, Mizoguchi F, Yonezaki N (eds) Software Security - Theories and Systems. Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, pp 174\u2013191 (2004). https:\/\/doi.org\/10.1007\/978-3-540-37621-7_9","DOI":"10.1007\/978-3-540-37621-7_9"},{"issue":"5","key":"504_CR59","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/1095430.1081750","volume":"30","author":"K Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. ACM SIGSOFT Software Engineering Notes 30(5), 263\u2013272 (2005). https:\/\/doi.org\/10.1145\/1095430.1081750","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"504_CR60","doi-asserted-by":"publisher","unstructured":"Shemer, R., Gurfinkel, A., Shoham, S., et\u00a0al.: Property Directed Self Composition. In: Dillig I, Tasiran S (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 161\u2013179 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"504_CR61","doi-asserted-by":"publisher","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, New York, NY, USA, PLDI \u201916, pp 57\u201369 (2016). https:\/\/doi.org\/10.1145\/2908080.2908092","DOI":"10.1145\/2908080.2908092"},{"key":"504_CR62","doi-asserted-by":"publisher","unstructured":"Staats, M., P\u01ces\u01cereanu, C.: Parallel symbolic execution for structural test generation. In: Proceedings of the 19th international symposium on Software testing and analysis. Association for Computing Machinery, New York, NY, USA, ISSTA \u201910, pp 183\u2013194 (2010). https:\/\/doi.org\/10.1145\/1831708.1831732","DOI":"10.1145\/1831708.1831732"},{"key":"504_CR63","doi-asserted-by":"publisher","unstructured":"Unno, H., Terauchi, T., Koskinen, E.: Constraint-Based Relational Verification. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification, pp. 742\u2013766. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_35","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"504_CR64","doi-asserted-by":"publisher","unstructured":"Yang, W., Vizel, Y., Subramanyan, P., et\u00a0al.: Lazy Self-composition for Security Verification. In: Chockler H, Weissenbacher G (eds) Computer Aided Verification. Springer International Publishing, Cham, Lecture Notes in Computer Science, pp 136\u2013156 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_11","DOI":"10.1007\/978-3-319-96142-2_11"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00504-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00504-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00504-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T09:14:32Z","timestamp":1765530872000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00504-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,27]]},"references-count":64,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["504"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00504-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,10,27]]},"assertion":[{"value":"29 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 August 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 October 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"40"}}