{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:28Z","timestamp":1784830768947,"version":"3.55.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Bounded model checking (BMC) is an effective technique for hunting bugs by incrementally exploring the state space of a system. To reason about infinite traces through a finite structure and to ultimately obtain completeness, BMC incorporates\n                    <jats:italic>loop conditions<\/jats:italic>\n                    that revisit previously observed states. This paper focuses on developing loop conditions for BMC of \u2013 a temporal logic for hyperproperties that allows expressing important policies for security and consistency in concurrent systems, etc. Loop conditions for  are more complicated than for , as different traces may loop inconsistently in unrelated moments. Existing BMC approaches for  only considered linear unrollings without any looping capability, which precludes both finding small infinite traces and obtaining a complete technique. We investigate loop conditions for  BMC, for  formulas that contain up to one quantifier alternation. We first present a general complete automata-based technique which is based on bounds of maximum unrollings. Then, we introduce alternative simulation-based algorithms that allow exploiting short loops effectively, generating SAT queries whose satisfiability guarantees the outcome of the original model checking problem. We also report empirical evaluation of the prototype implementation of our BMC techniques using .\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_4","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"66-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Efficient Loop Conditions for Bounded Model Checking Hyperproperties"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6277-2765","authenticated-orcid":false,"given":"Tzu-Han","family":"Hsu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0524-7390","authenticated-orcid":false,"given":"Sarai","family":"Sheinvald","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1800-5419","authenticated-orcid":false,"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253\u2013284, 1991.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Shreya Agrawal and Borzoo Bonakdarpour. Runtime verification of $$k$$-safety hyperproperties in HyperLTL. In Proc. of the 29th IEEE Computer Security Foundations Symp. (CSF\u201916), pages 239\u2013252. IEEE, 2016.","DOI":"10.1109\/CSF.2016.24"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Milo Martin, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, and Abhishek Udupa. Synthesizing finite-state protocols from scenarios and requirements. In Proc. of the 10th Int\u2019l Haifa Verification Conf. (HVC\u201914), volume 8855 of LNCS, pages 75\u201391. Springer, 2014.","DOI":"10.1007\/978-3-319-13338-6_7"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, Sylvain Heraud, C\u00e9sar Kunz, and Anne Pacalet. Implementing a direct method for certificate translation. In Proc. of the 11th Int\u2019l Conf. on Formal Engineering Methods (ICFEM\u201909), volume 5885 of LNCS, pages 541\u2013560. Springer, 2009.","DOI":"10.1007\/978-3-642-10373-5_28"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, and C\u00e9sar S\u00e1nchez. A temporal logic for asynchronous hyperproperties. In Proc. of the 33rd Int\u2019l Conf. on Computer Aided Verification (CAV\u201921), Part I, volume 12759 of LNCS, pages 694\u2013717. Springer, 2021.","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, and Joseph Sifakis. Property preserving simulations. In Proc. of the Fourth Int\u2019l Workshop on Computer Aided Verification (CAV\u201992), volume 663 of LNCS, pages 260\u2013273. Springer, 1992.","DOI":"10.1007\/3-540-56496-9_21"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. In Proc. of 35th IEEE Computer Security Foundations Symp. (CSF\u201922), pages 471\u2013485. IEEE, 2022.","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour, C\u00e9sar S\u00e1nchez, and Gerardo Schneider. Monitoring hyperproperties by combining static analysis and runtime verification. In Proc. of the 8th Int\u2019l Symp. on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA\u201918), Part II, volume 11245 of LNCS, pages 8\u201327. Springer, 2018.","DOI":"10.1007\/978-3-030-03421-4_2"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Laura Bozzelli, Adriano Peron, and C\u00e9sar S\u00e1nchez. Asynchronous extensions of HyperLTL. In Proc. of the 36th Annual ACM\/IEEE Symp. on Logic in Computer Science (LICS\u201921), pages 1\u201313. IEEE, 2021.","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Noel Brett, Umair Siddique, and Borzoo Bonakdarpour. Rewriting-based runtime verification for alternation-free HyperLTL. In Proc. of the 23rd Int\u2019l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201917), Part II, volume 10206 of LNCS, pages 77\u201393. Springer, 2017.","DOI":"10.1007\/978-3-662-54580-5_5"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Edmund\u00a0M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design (FMSD), 19(1):7\u201334, 2001.","DOI":"10.1023\/A:1011276507260"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Michael\u00a0R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher\u00a0K. Micinski, Markus\u00a0N. Rabe, and C\u00e9sar S\u00e1nchez. Temporal logics for hyperproperties. In Proc. of the 3rd Int\u2019l Conf. on Principles of Security and Trust (POST\u201914), volume 8414 of LNCS, pages 265\u2013284. Springer, 2014.","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Michael\u00a0R. Clarkson and Fred\u00a0B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157\u20131210, 2010.","DOI":"10.3233\/JCS-2009-0393"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Norine Coenen, Bernd Finkbeiner, C\u00e9sar S\u00e1nchez, and Leander Tentrup. Verifying hyperliveness. In Proc. of the 31st Int\u2019l Conf. on Computer Aided Verification (CAV\u201919), volume 11561 of LNCS, pages 121\u2013139. Springer, 2019.","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Leonardo\u00a0M. de\u00a0Moura and Nikolaj Bj\u00f8rner. Z3: An efficient SMT solver. In Proc. of 14th Int\u2019l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908), volume 4963 of LNCS, pages 337\u2013340. Springer, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, and Tobias Hans. MGHyper: Checking satisfiability of HyperLTL formulas beyond the $$\\exists ^*\\forall ^*$$ fragment. In Proc. of the 16th Int\u2019l Symp. on Automated Technology for Verification and Analysis (ATVA\u201918), volume 11138 of LNCS, pages 521\u2013527. Springer, 2018.","DOI":"10.1007\/978-3-030-01090-4_31"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, and Marvin Stenger. EAHyper: Satisfiability, implication, and equivalence checking of hyperproperties. In Proc. of the 29th Int\u2019l Conf. on Computer Aided Verification (CAV\u201917), Part II, volume 10427 of LNCS, pages 564\u2013570. Springer, 2017.","DOI":"10.1007\/978-3-319-63390-9_29"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A runtime verification tool for temporal hyperproperties. In Proc. of the 24th Int\u2019l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918), Part II, volume 10806 of LNCS, pages 194\u2013200. Springer, 2018.","DOI":"10.1007\/978-3-319-89963-3_11"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods in System Design (FMSD), 54(3):336\u2013363, 2019.","DOI":"10.1007\/s10703-019-00334-z"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, and Hazem Torfah. Model checking quantitative hyperproperties. In Proc. of the 30th Int\u2019l Conf. on Computer Aided Verification (CAV\u201918), Part I, volume 10981 of LNCS, pages 144\u2013163. Springer, 2018.","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Christian M\u00fcller, Helmut Seidl, and Eugene Zalinescu. Verifying security policies in multi-agent workflows with loops. In Proc. of the 15th ACM Conf. on Computer and Communications Security (CCS\u201917), pages 633\u2013645. ACM, 2017.","DOI":"10.1145\/3133956.3134080"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Markus\u00a0N. Rabe, and C\u00e9sar S\u00e1nchez. Algorithms for model checking HyperLTL and HyperCTL*. In Proc. of the 27th Int\u2019l Conf. on Computer Aided Verification (CAV\u201915), Part I, volume 9206 of LNCS, pages 30\u201348. Springer, 2015.","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Ohad Goudsmid, Orna Grumberg, and Sarai Sheinvald. Compositional model checking for multi-properties. In Proc. of the 22nd Int\u2019l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201921), volume 12597 of LNCS, pages 55\u201380. Springer, 2021.","DOI":"10.1007\/978-3-030-67067-2_4"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Orna Grumberg and David\u00a0E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(3):843\u2013871, 1994.","DOI":"10.1145\/177492.177725"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Jens\u00a0Oliver Gutsfeld, Markus M\u00fcller-Olm, and Christoph Ohrem. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang., 5:1\u201329, 2021.","DOI":"10.1145\/3434319"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Cristopher Hahn, Marvin Stenger, and Leander Tentrup. Constraint-based monitoring of hyperproperties. In Proc. of the 25th Int\u2019l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201919), volume 11428 of LNCS, pages 115\u2013131. Springer, 2019.","DOI":"10.1007\/978-3-030-17465-1_7"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Tzu-Han Hsu, C\u00e9sar S\u00e1nchez, and Borzoo Bonakdarpour. Bounded model checking for hyperproperties. In Proc. of the 27th Int\u2019l Conf on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201921). Part I, volume 12651 of LNCS, pages 94\u2013112. Springer, 2021.","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"4_CR28","unstructured":"Tzu-Han Hsu, C\u00e9sar S\u00e1nchez, Sarai Sheinvald, and Borzoo Bonakdarpour. Efficient loop conditions for bounded model checking hyperproperties. CoRR, abs\/2301.06209, 2023."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Orna Kupferman and Moshe\u00a0Y. Vardi. Model checking of safety properties. In Proc. of the 11th Int\u2019l Conf. on Computer Aided Verification (CAV\u201999), volume 1633 of LNCS, pages 172\u2013183. Springer, 1999.","DOI":"10.1007\/3-540-48683-6_17"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Kedar\u00a0S. Namjoshi and Lucas\u00a0M. Tabajara. Witnessing secure compilation. In Proc. of the 21st Int\u2019l Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201920), volume 11990 of LNCS, pages 1\u201322. Springer, 2020.","DOI":"10.1007\/978-3-030-39322-9_1"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The temporal logic of programs. In Proc. of the 18th Symp. on Foundations of Computer Science (FOCS\u201977), pages 46\u201357. IEEE, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Proc. of Current Trends in Concurrency, Overviews and Tutorials, volume 224 of LNCS, pages 510\u2013584. Springer, 1985.","DOI":"10.1007\/BFb0027047"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Sandro Stucki, C\u00e9sar S\u00e1nchez, Gerardo Schneider, and Borzoo Bonakdarpour. Graybox monitoring of hyperproperties. In Proc. of the 23rd Int\u2019l Symp. on Formal Methods (FM\u201919), volume 11800 of LNCS, pages 406\u2013424. Springer, 2019.","DOI":"10.1007\/978-3-030-30942-8_25"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Moshe\u00a0Y. Vardi and Pierre Wolper. Automata theoretic techniques for modal logic of programs. Journal of Computer and System Sciences, 32(2):183\u2013221, 1986.","DOI":"10.1016\/0022-0000(86)90026-7"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:04:38Z","timestamp":1781024678000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}