{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:54:10Z","timestamp":1770292450524,"version":"3.49.0"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572487","type":"print"},{"value":"9783031572494","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of<jats:italic>k<\/jats:italic>-safety properties, i.e., properties that state that all<jats:italic>k<\/jats:italic>-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\forall ^k\\exists ^l$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msup><mml:mo>\u2200<\/mml:mo><mml:mi>k<\/mml:mi><\/mml:msup><mml:msup><mml:mo>\u2203<\/mml:mo><mml:mi>l<\/mml:mi><\/mml:msup><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>properties, which state that for all<jats:italic>k<\/jats:italic>executions, there exist<jats:italic>l<\/jats:italic>executions that, together, satisfy a property. This captures important non-<jats:italic>k<\/jats:italic>-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\forall ^k\\exists ^l$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msup><mml:mo>\u2200<\/mml:mo><mml:mi>k<\/mml:mi><\/mml:msup><mml:msup><mml:mo>\u2203<\/mml:mo><mml:mi>l<\/mml:mi><\/mml:msup><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called and report on encouraging experimental results.<\/jats:p>","DOI":"10.1007\/978-3-031-57249-4_10","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:02:35Z","timestamp":1712214155000},"page":"196-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Automated Software Verification of Hyperliveness"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6234-5651","authenticated-orcid":false,"given":"Raven","family":"Beutner","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., H\u00e4hnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Softw. Syst. Model. (2005). https:\/\/doi.org\/10.1007\/s10270-004-0058-x","DOI":"10.1007\/s10270-004-0058-x"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90056-0","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Antonopoulos, T., Koskinen, E., Le, T.C., Nagasamudram, R., Naumann, D.A., Ngo, M.: An algebra of alignment for relational verification. Proc. ACM Program. Lang. (POPL) (2023). https:\/\/doi.org\/10.1145\/3571213","DOI":"10.1145\/3571213"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting semantics and its application to static analysis of information flow. In: Symposium on Principles of Programming Languages, POPL 2017 (2017). https:\/\/doi.org\/10.1145\/3009837.3009889","DOI":"10.1145\/3009837.3009889"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: Asymmetric product programs for relational program verification. In: International Symposium on Logical Foundations of Computer Science, LFCS 2013 (2013). https:\/\/doi.org\/10.1007\/978-3-642-35722-0_3","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. (2011). https:\/\/doi.org\/10.1017\/S0960129511000193","DOI":"10.1017\/S0960129511000193"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Symposium on Principles of Programming Languages, POPL 2004 (2004). https:\/\/doi.org\/10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Beringer, L.: Relational decomposition. In: International Conference on Interactive Theorem Proving, ITP 2011 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_6","DOI":"10.1007\/978-3-642-22863-6_6"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Beutner, R.: ForEx: Automated Software Verification of Hyperliveness (2023). https:\/\/doi.org\/10.5281\/zenodo.10436583","DOI":"10.5281\/zenodo.10436583"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Beutner, R.: Automated software verification of hyperliveness. CoRR (2024)","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: Computer Security Foundations Symposium, CSF 2022 (2022). https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: International Conference on Computer Aided Verification, CAV 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_17","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"10_CR13","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, TACAS 2023 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Model checking omega-regular hyperproperties with AutoHyperQ. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023 (2023). https:\/\/doi.org\/10.29007\/1XJT","DOI":"10.29007\/1XJT"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Second-order hyperproperties. In: International Conference on Computer Aided Verification, CAV 2023 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_15","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Biewer, S., Dimitrova, R., Fries, M., Gazda, M., Heinze, T., Hermanns, H., Mousavi, M.R.: Conformance relations and hyperproperties for doping detection in time and space. Log. Methods Comput. Sci. (2022). https:\/\/doi.org\/10.46298\/lmcs-18(1:14)2022","DOI":"10.46298\/lmcs-18(1:14)2022"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Bruni, R., Giacobazzi, R., Gori, R., Ranzato, F.: A correctness and incorrectness program logic. J. ACM (2023). https:\/\/doi.org\/10.1145\/3582267","DOI":"10.1145\/3582267"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM (2012). https:\/\/doi.org\/10.1145\/2240236.2240262","DOI":"10.1145\/2240236.2240262"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Chen, J., Feng, Y., Dillig, I.: Precise detection of side-channel vulnerabilities using quantitative cartesian hoare logic. In: Conference on Computer and Communications Security, CCS 2017 (2017). https:\/\/doi.org\/10.1145\/3133956.3134058","DOI":"10.1145\/3133956.3134058"},{"key":"10_CR20","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 om Principles of Security and Trust, POST 2014 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: International Conference on Computer Aided Verification, CAV 2019 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. (1978). https:\/\/doi.org\/10.1137\/0207005","DOI":"10.1137\/0207005"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Calculational design of [in]correctness transformational program logics by abstract interpretation. Proc. ACM Program. Lang. (POPL) (2024)","DOI":"10.1145\/3632849"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Dardinier, T., M\u00fcller, P.: Hyper hoare logic: (dis-)proving programhyperproperties. CoRR (2023). https:\/\/doi.org\/10.48550\/arXiv.2301.10037","DOI":"10.48550\/arXiv.2301.10037"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Dickerson, R., Ye, Q., Zhang, M.K., Delaware, B.: RHLE: modular deductive verification of relational $$\\forall \\exists $$ properties. In: Asian Symposium on Programming Languages and Systems, APLAS 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-21037-2_4","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"10_CR27","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science, Springer (1990). https:\/\/doi.org\/10.1007\/978-1-4612-3228-5","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"D\u2019Osualdo, E., Farzan, A., Dreyer, D.: Proving hypersafety compositionally. Proc. ACM Program. Lang. (OOPSLA) (2022). https:\/\/doi.org\/10.1145\/3563298","DOI":"10.1145\/3563298"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Eilers, M., M\u00fcller, P., Hitz, S.: Modular product programs. ACM Trans. Program. Lang. Syst. (2020). https:\/\/doi.org\/10.1145\/3324783","DOI":"10.1145\/3324783"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Farina, G.P., Chong, S., Gaboardi, M.: Relational symbolic execution. In: International Symposium on Principles and Practice of Programming Languages, PPDP 2019 (2019). https:\/\/doi.org\/10.1145\/3354166.3354175","DOI":"10.1145\/3354166.3354175"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Farzan, A., Vandikas, A.: Automated hypersafety verification. In: International Conference on Computer Aided Verification, CAV 2019 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_11","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Farzan, A., Vandikas, A.: Reductions for safety proofs. Proc. ACM Program. Lang. (POPL) (2020). https:\/\/doi.org\/10.1145\/3371081","DOI":"10.1145\/3371081"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^{*}$$. In: International Conference on Computer Aided Verification, CAV 2015 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: International Symposium of Formal Methods Europe, FME 2001 (2001). https:\/\/doi.org\/10.1007\/3-540-45251-6_29","DOI":"10.1007\/3-540-45251-6_29"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. Program Verification: Fundamental Issues in Computer Science (1993)","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"10_CR36","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: Symposium on Principles of Programming Languages, POPL 2004 (2004). https:\/\/doi.org\/10.1145\/964001.964021","DOI":"10.1145\/964001.964021"},{"key":"10_CR37","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM (1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"10_CR38","doi-asserted-by":"publisher","unstructured":"Hsu, T., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"Itzhaky, S., Shoham, S., Vizel, Y.: Hyperproperty verification as CHCsatisfiability. CoRR (2023). https:\/\/doi.org\/10.48550\/arXiv.2304.12588","DOI":"10.48550\/arXiv.2304.12588"},{"key":"10_CR40","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, M., Seidl, H., Finkbeiner, B.: Relational abstract interpretation for the verification of 2-hypersafety properties. In: Conference on Computer and Communications Security, CCS 2013 (2013). https:\/\/doi.org\/10.1145\/2508859.2516721","DOI":"10.1145\/2508859.2516721"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"Maksimovic, P., Cronj\u00e4ger, C., L\u00f6\u00f6w, A., Sutherland, J., Gardner, P.: Exact separation logic: Towards bridging the gap between verification and bug-finding. In: European Conference on Object-Oriented Programming, ECOOP 2023 (2023). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2023.19","DOI":"10.4230\/LIPICS.ECOOP.2023.19"},{"key":"10_CR43","doi-asserted-by":"publisher","unstructured":"Mastroeni, I., Pasqua, M.: Verifying bounded subset-closed hyperproperties. In: International Symposium on Static Analysis, SAS 2018 (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_17","DOI":"10.1007\/978-3-319-99725-4_17"},{"key":"10_CR44","doi-asserted-by":"publisher","unstructured":"Mastroeni, I., Pasqua, M.: Statically analyzing information flows: an abstract interpretation-based hyperanalysis for non-interference. In: Symposium on Applied Computing, SAC 2019 (2019). https:\/\/doi.org\/10.1145\/3297280.3297498","DOI":"10.1145\/3297280.3297498"},{"key":"10_CR45","doi-asserted-by":"publisher","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Symposium on Security and Privacy, SP 1988. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SECPRI.1988.8110","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"10_CR46","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_CR47","doi-asserted-by":"publisher","unstructured":"M\u00f6ller, B., O\u2019Hearn, P.W., Hoare, T.: On algebra of program correctness and incorrectness. In: International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2021 (2021). https:\/\/doi.org\/10.1007\/978-3-030-88701-8_20","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"10_CR48","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10_CR49","doi-asserted-by":"publisher","unstructured":"Nagasamudram, R., Naumann, D.A.: Alignment completeness for relational hoare logics. In: Symposium on Logic in Computer Science, LICS 2021 (2021). https:\/\/doi.org\/10.1109\/LICS52264.2021.9470690","DOI":"10.1109\/LICS52264.2021.9470690"},{"key":"10_CR50","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. (POPL) (2020). https:\/\/doi.org\/10.1145\/3371078","DOI":"10.1145\/3371078"},{"key":"10_CR51","doi-asserted-by":"publisher","unstructured":"Pasareanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: International Workshop on Model Checking Software, SPIN 2004 (2004). https:\/\/doi.org\/10.1007\/978-3-540-24732-6_13","DOI":"10.1007\/978-3-540-24732-6_13"},{"key":"10_CR52","doi-asserted-by":"publisher","unstructured":"Raad, A., Berdine, J., Dang, H., Dreyer, D., O\u2019Hearn, P.W., Villard, J.: Local reasoning about the presence of bugs: Incorrectness separation logic. In: International Conference on Computer Aided Verification, CAV 2020 (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_14","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"10_CR53","doi-asserted-by":"publisher","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: International Conference on Computer Aided Verification, CAV 2014 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_6","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"10_CR54","doi-asserted-by":"publisher","unstructured":"Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: European Symposium on Programming Languages and Systems, ESOP 2013 (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_31","DOI":"10.1007\/978-3-642-37036-6_31"},{"key":"10_CR55","doi-asserted-by":"publisher","unstructured":"Shemer, R., Gurfinkel, A., Shoham, S., Vizel, Y.: Property directed self composition. In: International Conference on Computer Aided Verification, CAV 2019 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"10_CR56","doi-asserted-by":"publisher","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: Conference on Programming Language Design and Implementation, PLDI 2016 (2016). https:\/\/doi.org\/10.1145\/2908080.2908092","DOI":"10.1145\/2908080.2908092"},{"key":"10_CR57","doi-asserted-by":"publisher","unstructured":"Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational verification. In: International Conference on Computer Aided Verification, CAV 2021 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_35","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"10_CR58","doi-asserted-by":"publisher","unstructured":"de Vries, E., Koutavas, V.: Reverse hoare logic. In: International Conference on Software Engineering and Formal Methods, SEFM 2011. LNCS (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_12","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"10_CR59","doi-asserted-by":"publisher","unstructured":"Wirth, N.: Program development by stepwise refinement. Commun. ACM (1971). https:\/\/doi.org\/10.1145\/362575.362577","DOI":"10.1145\/362575.362577"},{"key":"10_CR60","doi-asserted-by":"publisher","unstructured":"Yang, H.: Relational separation logic. Theor. Comput. Sci. (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.036","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"10_CR61","doi-asserted-by":"publisher","unstructured":"Zhang, K., Yin, X., Zamani, M.: Opacity of nondeterministic transition systems: A (bi)simulation relation approach. IEEE Trans. Autom. Control. (2019). https:\/\/doi.org\/10.1109\/TAC.2019.2908726","DOI":"10.1109\/TAC.2019.2908726"},{"key":"10_CR62","doi-asserted-by":"publisher","unstructured":"Zilberstein, N., Dreyer, D., Silva, A.: Outcome logic: A unifying foundation for correctness and incorrectness reasoning. Proc. ACM Program. Lang. (OOPSLA) (2023). https:\/\/doi.org\/10.1145\/3586045","DOI":"10.1145\/3586045"}],"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-57249-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:15:53Z","timestamp":1731690953000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57249-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572487","9783031572494"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57249-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"159","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":"53","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":"16","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":"33% - 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":"10","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)"}}]}}