{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,14]],"date-time":"2026-10-14T22:47:43Z","timestamp":1792018063753,"version":"4.4.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper introduces a bounded model checking (BMC) algorithm for <jats:italic>hyperproperties<\/jats:italic> expressed in HyperLTL, which \u2014 to the best of our knowledge \u2014 is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. Our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. We report on successful and efficient model checking, implemented in our tool called , of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and mutation testing.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_6","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"94-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":35,"title":["Bounded Model Checking for 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-0003-1800-5419","authenticated-orcid":false,"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"6_CR1","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 Symposium (CSF\u201916), pages 239\u2013252. IEEE, 2016.","DOI":"10.1109\/CSF.2016.24"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour and Bernd Finkbeiner. The complexity of monitoring hyperproperties. In Proc. of the IEEE 31st Computer Security Foundations Symposium (CSF\u201918), pages 162\u2013174. IEEE, 2018.","DOI":"10.1109\/CSF.2018.00019"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour and Bernd Finkbeiner. Program repair for hyperproperties. In Proc. of the 17th Symposium on Automated Technology for Verification and Analysis (ATVA\u201919), volume 11781 of LNCS, pages 423\u2013441. Springer, 2019.","DOI":"10.1007\/978-3-030-31784-3_25"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour and Bernd Finkbeiner. Controller synthesis for hyperproperties. In Proc. of the 33rd IEEE Computer Security Foundations Symposium (CSF\u201920), pages 366\u2013379. IEEE, 2020.","DOI":"10.1109\/CSF49147.2020.00033"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour, Pavithra Prabhakar, and C\u00e9sar S\u00e1nchez. Model checking timed hyperproperties in discrete-time systems. In Proc. of the 12th NASA Formal Methods Symposium (NFM\u201920), volume 12229 of LNCS, pages 311\u2013328. Springer, 2020.","DOI":"10.1007\/978-3-030-55754-6_18"},{"key":"6_CR6","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 Symposium 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":"6_CR7","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":"6_CR8","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, 19(1):7\u201334, 2001.","DOI":"10.1023\/A:1011276507260"},{"key":"6_CR9","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":"6_CR10","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":"6_CR11","doi-asserted-by":"crossref","unstructured":"Norine Coenen, Bernd Finkbeiner, Cristopher Hahn, and Jana Hofmann. The hierarchy of hyperlogics. In Proc. of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201919), pages 1\u201313. IEEE, 2019.","DOI":"10.1109\/LICS.2019.8785713"},{"key":"6_CR12","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), Part I, volume 11561 of LNCS, pages 121\u2013139. Springer, 2019.","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"6_CR13","unstructured":"Leonardo de\u00a0Moura and Nikolaj Bjorner. Z3 \u2013 a tutorial. Technical report, Microsoft, 2012."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Simon Doherty, David Detlefs, Lindsay Groves, Christine\u00a0H. Flood, Victor Luchangco, Paul\u00a0Alan Martin, Mark Moir, Nir Shavit, and Guy L.\u00a0Steele Jr. DCAS is not a silver bullet for nonblocking algorithm design. In Proc. of the 16th Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA\u201904), pages 216\u2013224. ACM, 2004.","DOI":"10.1145\/1007912.1007945"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Andreas Fellner, Mitra\u00a0Tabaei Befrouei, and Georg Weissenbacher. Mutation testing with hyperproperties. In Proc. of the 17th Int\u2019l Conf. on Software Engineering and Formal Methods (SEFM\u201919), volume 11724 of LNCS, pages 203\u2013221. Springer, 2019.","DOI":"10.1007\/978-3-030-30446-1_11"},{"key":"6_CR16","unstructured":"Bernd Finkbeiner and Cristopher Hahn. Deciding hyperproperties. In Proc. of the 27th Int\u2019l Conf. on Concurrency Theory (CONCUR\u201916), volume\u00a059 of LIPIcs, pages 13:1\u201313:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2016."},{"key":"6_CR17","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 Symposium 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":"6_CR18","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137\u2013163, 2020.","DOI":"10.1007\/s00236-019-00358-2"},{"key":"6_CR19","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":"6_CR20","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":"6_CR21","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner, Cristopher Hahn, Marvin Stenger, and Leander Tentrup. Monitoring hyperproperties. Formal Methods in System Design, 54(3):336\u2013363, 2019.","DOI":"10.1007\/s10703-019-00334-z"},{"key":"6_CR22","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":"6_CR23","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":"6_CR24","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":"6_CR25","doi-asserted-by":"crossref","unstructured":"Joseph\u00a0A. Goguen and Jos\u00e9 Meseguer. Security policies and security models. In 1982 IEEE Symposium on Security and Privacy, pages 11\u201320. IEEE Computer Society, 1982.","DOI":"10.1109\/SP.1982.10014"},{"key":"6_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":"6_CR27","doi-asserted-by":"crossref","unstructured":"Klaus Havelund and Doron Peled. Runtime verification: From propositional to first-order temporal logic. In Proc. of the 18th Int\u2019l Conf. on Runtime Verification (RV\u201918), volume 11237 of LNCS, pages 90\u2013112. Springer, 2018.","DOI":"10.1007\/978-3-030-03769-7_7"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Jesko Hecking-Harbusch and Leander Tentrup. Solving QBF by abstraction. In Proc. of the 9th Int\u2019l Symposium on Games, Automata, Logics and Formal Verification (GandALF\u201918), volume 277 of EPTCS, pages 88\u2013102, 2018.","DOI":"10.4204\/EPTCS.277.7"},{"key":"6_CR29","unstructured":"Maurice Herlihy and Jeannette\u00a0M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems, 12(3):463\u2013492, 1990."},{"key":"6_CR30","unstructured":"Tzu-Han Hsu, C\u00e9sar S\u00e1nchez, and Borzoo Bonakdarpour. Bounded model checking for hyperproperties. CoRR, abs\/2009.08907, 2020."},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Wojciech Jamroga, Sjouke Mauw, and Matthijs Melissen. Fairness in non-repudiation protocols. In Proc. of the 7th Int\u2019l Workshop on Security and Trust Management (STM\u201911), volume 7170 of LNCS, pages 122\u2013139. Springer, 2011.","DOI":"10.1007\/978-3-642-29963-6_10"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Geoffrey Smith and Dennis\u00a0M. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. of the 25th ACM Symposium on Principles of Programming Languages (POPL\u201998), pages 355\u2013364. ACM, 1998.","DOI":"10.1145\/268946.268975"},{"key":"6_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 Symposium on Formal Methods (FM\u201919), volume 11800 of LNCS, pages 406\u2013424. Springer, 2019.","DOI":"10.1007\/978-3-030-30942-8_25"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Yu Wang, Siddharta Nalluri, and Miroslav Pajic. Hyperproperties for robotics: Planning via HyperLTL. In 2020 IEEE Int\u2019l Conf. on Robotics and Automation (ICRA\u201920), pages 8011\u20138017. IEEE, 2020.","DOI":"10.1109\/ICRA40945.2020.9196874"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Yu\u00a0Wang, Mojtaba Zarei, Borzoo Bonakdarpour, and Miroslav Pajic. Statistical verification of hyperproperties for cyber-physical systems. ACM Transactions on Embedded Computing systems, 18(5s):92:1\u201392:23, 2019.","DOI":"10.1145\/3358232"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T00:04:39Z","timestamp":1616371479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}