{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:13Z","timestamp":1784793793241,"version":"3.55.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper presents the first symbolic bounded model checking technique capable of verifying\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\forall ^+\\exists ^+$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mrow>\n                            <mml:msup>\n                              <mml:mo>\u2200<\/mml:mo>\n                              <mml:mo>+<\/mml:mo>\n                            <\/mml:msup>\n                            <mml:msup>\n                              <mml:mo>\u2203<\/mml:mo>\n                              <mml:mo>+<\/mml:mo>\n                            <\/mml:msup>\n                          <\/mml:mrow>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -liveness hyperproperties (expressed in HyperLTL) over arbitrary (non-terminating) reactive systems. Previous bounded procedures for HyperLTL handled only safety hyperproperties or arbitrary properties over terminating systems. We implement our technique as\n                    <jats:sc>HyperLasso<\/jats:sc>\n                    . Our evaluation results show that it consistently outperforms the explicit-state complete model checker\n                    <jats:sc>AutoHyper<\/jats:sc>\n                    (the only existing tool capable of automatically verifying this class of problems) at several complex bug-finding and synthesis problems.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_24","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:38Z","timestamp":1784791058000},"page":"473-496","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["HyperLasso: Bounded Model Checking of\u00a0$$\\forall ^+\\exists ^+$$-Liveness Hyperproperties"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2714-8027","authenticated-orcid":false,"given":"Alcino","family":"Cunha","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0720-7744","authenticated-orcid":false,"given":"Hugo","family":"Pacheco","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"24_CR1","unstructured":"Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories. Edinburgh, UK. vol. 13, p. 14 (2010). https:\/\/smt-lib.org\/papers\/smt-lib-reference-v2.7-r2025-07-07.pdf"},{"issue":"6","key":"24_CR2","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1109\/CSFW.2004.1310735","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011). https:\/\/doi.org\/10.1109\/CSFW.2004.1310735","journal-title":"Math. Struct. Comput. Sci."},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/978-3-030-81685-8_33","volume-title":"Computer Aided Verification","author":"J Baumeister","year":"2021","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 694\u2013717. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_33"},{"key":"24_CR4","doi-asserted-by":"publisher","unstructured":"Beutner, R.: Automated software verification of hyperliveness. In: TACAS (2). LNCS, vol. 14571, pp. 196\u2013216. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57249-4_10","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"24_CR5","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: CSF, pp. 471\u2013485. IEEE (2022). https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"24_CR6","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: explicit-state model checking for HyperLTL. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 145\u2013163. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"24_CR7","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Model checking omega-regular hyperproperties with AutoHyperQ. In: LPAR. EPiC Series in Computing, vol. 94, pp. 23\u201335. EasyChair (2023).https:\/\/doi.org\/10.29007\/1xjt","DOI":"10.29007\/1xjt"},{"issue":"2","key":"24_CR8","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/s10703-025-00482-5","volume":"66","author":"R Beutner","year":"2025","unstructured":"Beutner, R., Finkbeiner, B.: Predicate abstraction for hyperliveness verification. Formal Methods Syst. Des. 66(2), 238\u2013277 (2025). https:\/\/doi.org\/10.1007\/s10703-025-00482-5","journal-title":"Formal Methods Syst. Des."},{"key":"24_CR9","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Verifying asynchronous hyperproperties in reactive systems. Proc. ACM Program. Lang. 9(OOPSLA2) (2025). https:\/\/doi.org\/10.1145\/3763130","DOI":"10.1145\/3763130"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"24_CR11","doi-asserted-by":"publisher","unstructured":"Bombardelli, A., Bozzelli, L., Sanchez, C., Tonetta, S.: (Asynchronous) temporal logics for hyperproperties on finite traces. In: International Symposium on Model Checking Software, pp. 25\u201343. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-06847-7_2","DOI":"10.1007\/978-3-032-06847-7_2"},{"key":"24_CR12","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The NUXMV symbolic model checker. In: International Conference on Computer Aided Verification, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"24_CR13","unstructured":"Cavada, R., et al.: NuSMV 2.6 user manual. FBK-IRST (2010). http:\/\/nusmv.fbk.eu\/NuSMV\/userman\/v26\/nusmv.pdf"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM (JACM) 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","DOI":"10.1145\/876638.876643"},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: International Conference on Principles of Security and Trust, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"24_CR16","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: International Conference on Computer Aided Verification, pp. 121\u2013139. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"issue":"OOPSLA2","key":"24_CR18","doi-asserted-by":"publisher","first-page":"1420","DOI":"10.1145\/3689761","volume":"8","author":"A Correnson","year":"2024","unstructured":"Correnson, A., Nie\u00dfen, T., Finkbeiner, B., Weissenbacher, G.: Finding $$\\forall $$$$\\exists $$ hyperbugs using symbolic execution. Proc. ACM Program. Lang. 8(OOPSLA2), 1420\u20131445 (2024). https:\/\/doi.org\/10.1145\/3689761","journal-title":"Proc. ACM Program. Lang."},{"key":"24_CR19","doi-asserted-by":"publisher","unstructured":"Crooks, N., Pu, Y., Alvisi, L., Clement, A.: Seeing is believing: a client-centric specification of database isolation. In: Proceedings of the ACM Symposium on Principles of Distributed Computing, pp. 73\u201382 (2017). https:\/\/doi.org\/10.1145\/3087801.3087802","DOI":"10.1145\/3087801.3087802"},{"issue":"OOPSLA2","key":"24_CR20","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. Proc. ACM Program. Lang. 8(OOPSLA2), 1279\u20131308 (2024). https:\/\/doi.org\/10.1145\/3689756","journal-title":"Proc. ACM Program. Lang."},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"24_CR22","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification, pp. 325\u2013332. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"24_CR23","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$ ^*$$. In: CAV (1). LNCS, vol. 9206, pp. 30\u201348. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"24_CR24","doi-asserted-by":"publisher","unstructured":"Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63\u201367 (1990). https:\/\/doi.org\/10.1016\/0020-0190(90)90107-9","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"24_CR25","doi-asserted-by":"publisher","unstructured":"Hsu, T., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: Bounded model checking for asynchronous hyperproperties. In: TACAS (1). LNCS, vol. 13993, pp. 29\u201346. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_2","DOI":"10.1007\/978-3-031-30823-9_2"},{"key":"24_CR26","unstructured":"Hsu, T.H., Rabizadeh, M., Rogale, K., Filippov, F., de Oliveira Batista, M.A., Bonakdarpour, B.: HyperQB 2.0: a bounded model checker for hyperproperties. In: International Conference on Computer Aided Verification. to appear (2026). https:\/\/arxiv.org\/abs\/2109.12989"},{"key":"24_CR27","doi-asserted-by":"publisher","unstructured":"Hsu, T.H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 94\u2013112. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"24_CR28","doi-asserted-by":"publisher","unstructured":"Hsu, T.H., S\u00e1nchez, C., Sheinvald, S., Bonakdarpour, B.: Efficient loop conditions for bounded model checking hyperproperties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 66\u201384. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_4","DOI":"10.1007\/978-3-031-30823-9_4"},{"key":"24_CR29","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Shoham, S., Vizel, Y.: Hyperproperty verification as CHC satisfiability. In: ESOP (2). LNCS, vol. 14577, pp. 212\u2013241. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57267-8_9","DOI":"10.1007\/978-3-031-57267-8_9"},{"key":"24_CR30","doi-asserted-by":"publisher","unstructured":"Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: CAV. LNCS, vol. 6806, pp. 557\u2013572. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_44","DOI":"10.1007\/978-3-642-22110-1_44"},{"key":"24_CR31","doi-asserted-by":"publisher","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem, pp. 171\u2013178. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3335772.3335782","DOI":"10.1145\/3335772.3335782"},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Lamport, L., Schneider, F.B.: Verifying hyperproperties with TLA. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pp. 1\u201316. IEEE (2021). https:\/\/doi.org\/10.1109\/CSF51468.2021.00012","DOI":"10.1109\/CSF51468.2021.00012"},{"key":"24_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-319-41540-6_7","volume-title":"Computer Aided Verification","author":"AW Lin","year":"2016","unstructured":"Lin, A.W., R\u00fcmmer, P.: Liveness of randomised parameterised systems under arbitrary schedulers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 112\u2013133. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_7"},{"key":"24_CR34","unstructured":"Macedo, N., Pacheco, H.: Model checking of hyperproperties for high-level relational models (2026). https:\/\/arxiv.org\/abs\/2512.12024"},{"key":"24_CR35","doi-asserted-by":"publisher","unstructured":"Smith, G., Volpano, D.M.: Secure information flow in a multi-threaded imperative language. In: POPL, pp. 355\u2013364. ACM (1998). https:\/\/doi.org\/10.1145\/268946.268975","DOI":"10.1145\/268946.268975"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:39Z","timestamp":1784791059000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}