{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:12Z","timestamp":1784793792328,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"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                    We introduce the tool\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$^{\\textsf {\\small 2.0}}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow\/>\n                            <mml:mrow>\n                              <mml:mstyle>\n                                <mml:mn>2<\/mml:mn>\n                              <\/mml:mstyle>\n                              <mml:mo>.<\/mml:mo>\n                              <mml:mn>0<\/mml:mn>\n                            <\/mml:mrow>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    , the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line, standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in  and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_26","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:34Z","timestamp":1784791114000},"page":"511-525","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["HyperQB 2.0: A Bounded Model Checker for\u00a0Hyperproperties"],"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\/0009-0007-6037-5911","authenticated-orcid":false,"given":"Milad","family":"Rabizadeh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6213-3933","authenticated-orcid":false,"given":"Kenneth","family":"Rogale","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fedor","family":"Filippov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco A.","family":"de Oliveira Batista","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":[[2026,7,24]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxp025","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. The MIT Press (2008). https:\/\/doi.org\/10.1093\/comjnl\/bxp025","journal-title":"The MIT Press"},{"key":"26_CR2","doi-asserted-by":"publisher","unstructured":"Baumeister, J., Coenen, N., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: A temporal logic for asynchronous hyperproperties. In: The 33rd International Conference on Computer Aided Verification (CAV), 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":"26_CR3","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: explicit-state model checking for HyperLTL. In: Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS), 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":"26_CR4","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., S\u00e1nchez, C., Schneider, G.: Monitoring hyperproperties by combining static analysis and runtime verification. In: Proceedings of the 8th Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 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":"26_CR5","doi-asserted-by":"publisher","unstructured":"Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Computer Aided Verification (CAV). LNCS, vol.\u00a06174, pp. 24\u201340. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"26_CR6","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: Nusmv: A new symbolic model verifier. In: International conference on computer aided verification, pp. 495\u2013499. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_44","DOI":"10.1007\/3-540-48683-6_44"},{"key":"26_CR7","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Design 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","DOI":"10.1023\/A:1011276507260"},{"key":"26_CR8","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: Proceedings of the 3rd Conference on Principles of Security and Trust POST, 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":"26_CR9","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":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-25540-4_7","volume-title":"Computer Aided Verification","author":"N Coenen","year":"2019","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7"},{"key":"26_CR11","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Torfah, H.: Model checking quantitative hyperproperties. In: Proceedings of the 30th International Conference on Computer Aided Verification, pp. 144\u2013163 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"26_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: Proceedings of the 27th International Conference on Computer Aided Verification (CAV), 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":"26_CR13","unstructured":"Gleissenthall, K.V., Kici, R.G., Stefan, D., Jhala, R.: Iodine: verifying constant-time execution of hardware. In: Proceedings of the 28th USENIX Conference on Security Symposium, pp. 1411\u20131428. SEC\u20192019, USENIX Association (2019)"},{"key":"26_CR14","unstructured":"GmbH, Y.: Yosys open synthesis suite. https:\/\/yosyshq.net\/yosys\/"},{"key":"26_CR15","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symp. on Security and Privacy, pp. 11\u201320 (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"issue":"3","key":"26_CR16","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR17","doi-asserted-by":"publisher","unstructured":"Hsu, T.H., Bonakdarpour, B., Finkbeiner, B., S\u00e1nchez, C.: Bounded model checking for asynchronous hyperproperties. In: Proceedings of the 29th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), 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":"26_CR18","doi-asserted-by":"publisher","unstructured":"Hsu, T.H., S\u00e1nchez, C., , Sheinvald, S., Bonakdarpour, B.: Efficient loop conditions for bounded model checking hyperproperties. In: Proceedings of the 29th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 66 \u2013 84 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_4","DOI":"10.1007\/978-3-031-30823-9_4"},{"key":"26_CR19","doi-asserted-by":"publisher","unstructured":"Hsu, T.H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 94\u2013112 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"26_CR20","doi-asserted-by":"publisher","unstructured":"Hsu, T.H., Rabizadeh, M., Rogale, K., Filippov, F., Batista, M.A., Bonakdarpour, B.: Hyperqb: A bounded model checker for hyperproperties. arXiv preprint arXiv:2109.12989 (2021). https:\/\/doi.org\/10.48550\/arXiv.2109.12989","DOI":"10.48550\/arXiv.2109.12989"},{"key":"26_CR21","unstructured":"IEEE: IEEE Standard for Verilog Hardware Description Language (2005). IEEE Std 1364-2005"},{"key":"26_CR22","unstructured":"Kroening, D.: Ebmc. https:\/\/www.cprover.org\/ebmc\/"},{"key":"26_CR23","unstructured":"Mermaid Contributors: Mermaid (2025). https:\/\/mermaid.js.org"},{"key":"26_CR24","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"26_CR25","doi-asserted-by":"publisher","unstructured":"Ryan, K., Sturton, C.: Sylvia: Countering the path explosion problem in the symbolic execution of hardware designs. In: Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 110\u2013121. FMCAD (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_19","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_19"},{"key":"26_CR26","doi-asserted-by":"publisher","unstructured":"Tentrup, L.: CAQE and quabs: Abstraction based QBF solvers. J. Satisfiability Boolean Model. Comput. 11(1), 155\u2013210 (2019). https:\/\/doi.org\/10.3233\/SAT190121","DOI":"10.3233\/SAT190121"},{"key":"26_CR27","doi-asserted-by":"publisher","unstructured":"Wang, Y., Zarei, M., Bonakdarpour, B., Pajic, M.: Statistical verification of hyperproperties for cyber-physical systems. ACM Trans. Embedded Comput. Syst. 18(5s), 92:1\u201392:23 (2019). https:\/\/doi.org\/10.1145\/3358232","DOI":"10.1145\/3358232"}],"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_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:38Z","timestamp":1784791118000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_26","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"}}]}}