{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T20:49:17Z","timestamp":1769719757889,"version":"3.49.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787492","type":"print"},{"value":"9783031787508","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-78750-8_10","type":"book-chapter","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:16:04Z","timestamp":1739276164000},"page":"198-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Satisfiability of\u00a0Hyperproperties Using First-Order Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6234-5651","authenticated-orcid":false,"given":"Raven","family":"Beutner","sequence":"first","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"}]}],"member":"297","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2024.3384448","author":"M Anand","year":"2024","unstructured":"Anand, M., Murali, V., Trivedi, A., Zamani, M.: Verification of hyperproperties for dynamical systems via barrier certificates. IEEE Trans. Autom. Control (2024). https:\/\/doi.org\/10.1109\/TAC.2024.3384448","journal-title":"IEEE Trans. Autom. Control"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"10_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C., et\u00a0al.: The SMT-lib standard: Version 2.0. In: International Workshop on Satisfiability Modulo Theories (2010)"},{"key":"10_CR4","unstructured":"Barwise, J.: An introduction to first-order logic. In: Studies in Logic and the Foundations of Mathematics (1977)"},{"key":"10_CR5","unstructured":"Beth, E.W.: Semantic entailment and formal derivability (1955)"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Beutner, R., Carral, D., Finkbeiner, B., Hofmann, J., Kr\u00f6tzsch, M.: Deciding hyperproperties combined with functional specifications. In: Symposium on Logic in Computer Science, LICS 2022 (2022). https:\/\/doi.org\/10.1145\/3531130.3533369","DOI":"10.1145\/3531130.3533369"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Biewer, S., et al.: Conformance relations and hyperproperties for doping detection in time and space. Log. Methods Comput. Sci. 18(1) (2022). https:\/\/doi.org\/10.46298\/LMCS-18(1:14)2022","DOI":"10.46298\/LMCS-18(1:14)2022"},{"key":"10_CR8","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: Workshop on Model Computation-Principles, Algorithms, Applications (2003)"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. In: Workshop on Quantitative Aspects of Programming Languages, QAPL 2004 (2004). https:\/\/doi.org\/10.1016\/J.ENTCS.2004.01.018","DOI":"10.1016\/J.ENTCS.2004.01.018"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Computer Security Foundations Symposium, CSF 2008 (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: Symposium on Logic in Computer Science, LICS 2019 (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"10_CR13","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (1960). https:\/\/doi.org\/10.1145\/321033.321034","journal-title":"J. ACM"},{"key":"10_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-13188-2_9","volume-title":"CAV 2022","author":"A Duret-Lutz","year":"2022","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13372, pp. 174\u2013187. Springer, Cham. (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: International Conference on Concurrency Theory, CONCUR 2016 (2016). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2016.13","DOI":"10.4230\/LIPICS.CONCUR.2016.13"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/978-3-030-01090-4_31","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Hans, T.: MGHyper: checking satisfiability of\u00a0HyperLTL formulas beyond the $$\\exists ^*\\forall ^*$$ fragment. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 521\u2013527. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_31"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-63390-9_29","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 564\u2013570. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_29"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des. (2019). https:\/\/doi.org\/10.1007\/S10703-019-00334-Z","DOI":"10.1007\/S10703-019-00334-Z"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: Symposium on Theoretical Aspects of Computer Science, STACS 2017 (2017). https:\/\/doi.org\/10.4230\/LIPICS.STACS.2017.30","DOI":"10.4230\/LIPICS.STACS.2017.30"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Fortin, M., Kuijer, L.B., Totzke, P., Zimmermann, M.: HyperLTL satisfiability is $$\\Sigma _1^1$$-complete, HyperCTL* satisfiability is $$\\Sigma _1^2$$-complete. In: International Symposium on Mathematical Foundations of Computer Science, MFCS 2021 (2021). https:\/\/doi.org\/10.4230\/LIPICS.MFCS.2021.47","DOI":"10.4230\/LIPICS.MFCS.2021.47"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Propositional dynamic logic for hyperproperties. In: International Conference on Concurrency Theory, CONCUR 2020 (2020). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2020.50","DOI":"10.4230\/LIPICS.CONCUR.2020.50"},{"key":"10_CR22","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (1990). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-030-72016-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T-H Hsu","year":"2021","unstructured":"Hsu, T.-H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: TACAS 2021. LNCS, vol. 12651, pp. 94\u2013112. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Janota, M., Suda, M.: Towards smarter MACE-style model finders. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2018 (2018). https:\/\/doi.org\/10.29007\/W42S","DOI":"10.29007\/W42S"},{"key":"10_CR25","unstructured":"Kamp, J.A.W.: Tense logic and the theory of linear order (1968)"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 172\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_17"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Mascle, C., Zimmermann, M.: The keys to decidable HyperLTL satisfiability: small models or very simple formulas. In: Conference on Computer Science Logic, CSL 2020 (2020). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2020.29","DOI":"10.4230\/LIPICS.CSL.2020.29"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Symposium on Security and Privacy, SP 1988 (1988). https:\/\/doi.org\/10.1109\/SECPRI.1988.8110","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"10_CR31","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: quasigroup existence problems. Technical report (1994)"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Symposium on Research in Security and Privacy, SP 1994 (1994). https:\/\/doi.org\/10.1109\/RISP.1994.296590","DOI":"10.1109\/RISP.1994.296590"},{"key":"10_CR33","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":"10_CR34","unstructured":"Rabe, M.N.: A temporal logic approach to information-flow control. Ph.D. thesis, Saarland University (2016)"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-39799-8_42","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2013","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 640\u2013655. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_42"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"key":"10_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 277\u2013291. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-69778-0_28"},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-642-00596-1_21","volume-title":"Foundations of Software Science and Computational Structures","author":"G Smith","year":"2009","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_21"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Automated Deduction \u2014 CADE-12","author":"G Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 252\u2013266. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_18"},{"key":"10_CR40","doi-asserted-by":"publisher","unstructured":"Sweeney, L.: k-anonymity: a model for protecting privacy. Int. J. Uncertain. Fuzziness Knowl. Based Syst. (2002). https:\/\/doi.org\/10.1142\/S0218488502001648","DOI":"10.1142\/S0218488502001648"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Wang, Y., Nalluri, S., Pajic, M.: Hyperproperties for robotics: planning via hyperltl. In: International Conference on Robotics and Automation, ICRA 2020 (2020). https:\/\/doi.org\/10.1109\/ICRA40945.2020.9196874","DOI":"10.1109\/ICRA40945.2020.9196874"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Computer Security Foundations Workshop, CSFW 2003 (2003). https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"10_CR43","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: International Joint Conference on Artificial Intelligence, IJCAI 1995 (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78750-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T10:08:26Z","timestamp":1769681306000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78750-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787492","9783031787508"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78750-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"12 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}