{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,5]],"date-time":"2026-05-05T02:47:34Z","timestamp":1777949254633,"version":"3.51.4"},"publisher-location":"Singapore","reference-count":51,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819578252","type":"print"},{"value":"9789819578269","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-981-95-7826-9_6","type":"book-chapter","created":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T22:38:37Z","timestamp":1777847917000},"page":"93-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Generic Dynamic Logic for\u00a0Program Reasoning Based on\u00a0Operational Semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0685-6905","authenticated-orcid":false,"given":"Yuanrui","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9888-6975","authenticated-orcid":false,"given":"Zhibin","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,1]]},"reference":[{"key":"6_CR1","unstructured":"https:\/\/github.com\/yrz5a\/setta2025-onlineReport.git"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Afshari, B., Enqvist, S., Leigh, G.E.: Cyclic proofs for the first-order $$\\upmu $$-calculus. Logic J. IGPL 32(1), 1\u201334 (2022)","DOI":"10.1093\/jigpal\/jzac053"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Dockins, R., et\u00a0al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-38574-2_22","volume-title":"Automated Deduction \u2013 CADE-24","author":"B Beckert","year":"2013","unstructured":"Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 315\u2013329. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_22"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-49812-6_3","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"B Beckert","year":"2016","unstructured":"Beckert, B., Klebanov, V., Wei\u00df, B.: Dynamic logic for Java. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 49\u2013106. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_3"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Benevides, M.R., Schechter, L.M.: A propositional dynamic logic for concurrent programs based on the $$\\pi $$-calculus. In: M4M 2009, pp. 49\u201364. Elsevier (2010)","DOI":"10.1016\/j.entcs.2010.04.005"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/3-540-15670-4_19","volume-title":"Seminar on Concurrency","author":"G Berry","year":"1985","unstructured":"Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 389\u2013448. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15670-4_19"},{"issue":"2","key":"6_CR8","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The ESTEREL synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87\u2013152 (1992)","journal-title":"Sci. Comput. Program."},{"key":"6_CR9","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"issue":"1","key":"6_CR10","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1328897.1328453","volume":"43","author":"J Brotherston","year":"2008","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. SIGPLAN Not. 43(1), 101\u2013112 (2008)","journal-title":"SIGPLAN Not."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Simpson, A.: Complete sequent calculi for induction and infinite descent. In: LICS 2007, pp. 51\u201362 (2007)","DOI":"10.1109\/LICS.2007.16"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Chen, X., Rosu, G.: Matching $$mu$$-logic. In: LICS 2019, pp. 1\u201313. IEEE Computer Society (2019)","DOI":"10.1109\/LICS.2019.8785675"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-09510-1_15","volume-title":"Automata, Languages and Programming","author":"N Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. In: Maurer, H.A. (ed.) ICALP 1979. LNCS, vol. 71, pp. 188\u2013202. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09510-1_15"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Do, C.M., Takagi, T., Ogata, K.: Automated quantum protocol verification based on concurrent dynamic quantum logic. ACM Trans. Softw. Eng. Methodol. (2024). Accepted","DOI":"10.1145\/3708475"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-29026-9_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S Docherty","year":"2019","unstructured":"Docherty, S., Rowe, R.N.S.: A non-wellfounded, labelled proof system for propositional dynamic logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 335\u2013352. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_19"},{"issue":"2","key":"6_CR16","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Gesell, M., Schneider, K.: A Hoare calculus for the verification of synchronous languages. In: PLPV 2012, pp. 37\u201348. Association for Computing Machinery (2012)","DOI":"10.1145\/2103776.2103782"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. The MIT Press, Cambridge (1996)","DOI":"10.7551\/mitpress\/1188.001.0001"},{"key":"6_CR19","unstructured":"Gutsfeld, J.O., M\u00fcller-Olm, M., Ohrem, C.: Propositional dynamic logic for hyperproperties. In: 31st International Conference on Concurrency Theory (CONCUR), pp. 50:1\u201350:22 (2020)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-030-30985-5_11","volume-title":"From Software Engineering to Formal Methods and Tools, and Back","author":"R Hennicker","year":"2019","unstructured":"Hennicker, R., Wirsing, M.: A generic dynamic logic with applications to interaction-based systems. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 172\u2013187. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30985-5_11"},{"issue":"10","key":"6_CR22","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Icard, B.: A dynamic logic for information evaluation in intelligence (2024). https:\/\/arxiv.org\/abs\/2405.19968","DOI":"10.2139\/ssrn.4627928"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Jones, E., Ong, C.H.L., Ramsay, S.: CycleQ: an efficient basis for cyclic equational reasoning. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2022, pp. 395\u2013409. Association for Computing Machinery, New York, NY, USA (2022)","DOI":"10.1145\/3519939.3523731"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-642-02716-1_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"N Jungteerapanich","year":"2009","unstructured":"Jungteerapanich, N.: A tableau system for the modal $$\\mu $$-calculus. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 220\u2013234. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_17"},{"issue":"2","key":"6_CR26","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic pdl. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-91265-9_4","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"X Li","year":"2021","unstructured":"Li, X., Zhang, Q., Wang, G., Shi, Z., Guan, Y.: Reasoning about iteration and recursion uniformly based on big-step semantics. In: Qin, S., Woodcock, J., Zhang, W. (eds.) SETTA 2021. LNCS, vol. 13071, pp. 61\u201380. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-91265-9_4"},{"issue":"7","key":"6_CR28","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Logic Algebr. Program. 81(7), 721\u2013781 (2012)","journal-title":"J. Logic Algebr. Program."},{"key":"6_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R Milner","year":"1982","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-10235-3"},{"issue":"1","key":"6_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, i. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-319-89884-1_21","volume-title":"Programming Languages and Systems","author":"B Moore","year":"2018","unstructured":"Moore, B., Pe\u00f1a, L., Rosu, G.: Program verification by coinduction. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 589\u2013618. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_21"},{"issue":"3\u20134","key":"6_CR32","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s00165-010-0153-4","volume":"22","author":"T Mossakowski","year":"2010","unstructured":"Mossakowski, T., Schr\u00f6der, L., Goncharov, S.: A generic complete dynamic logic for reasoning about purity and effects. Form. Asp. Comput. 22(3\u20134), 363\u2013384 (2010)","journal-title":"Form. Asp. Comput."},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL) (2019)","DOI":"10.1145\/3371078"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-031-17715-6_24","volume-title":"Theoretical Aspects of Computing - ICTAC 2022","author":"R Pardo","year":"2022","unstructured":"Pardo, R., Johnsen, E.B., et al.: A specification logic for programs in the probabilistic guarded command language. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC 2022. LNCS, vol. 13572, pp. 369\u2013387. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_24"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-73099-6_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Platzer","year":"2007","unstructured":"Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol. 4548, pp. 216\u2013232. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73099-6_17"},{"key":"6_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical Foundations of Cyber-Physical Systems","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"6_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 109\u2013121. IEEE Computer Society (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"6_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BFb0015471","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software","author":"W Reif","year":"1995","unstructured":"Reif, W.: The Kiv-approach to software verification. In: Broy, M., J\u00e4hnichen, S. (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. LNCS, vol. 1009, pp. 339\u2013368. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0015471"},{"key":"6_CR40","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"6_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-31585-5_33","volume-title":"Automata, Languages, and Programming","author":"G Ro\u015fu","year":"2012","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Towards a unified theory of operational and axiomatic semantics. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012. LNCS, vol. 7392, pp. 351\u2013363. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31585-5_33"},{"key":"6_CR42","doi-asserted-by":"crossref","unstructured":"Rosu, G., Stefanescu, A., Ciob\u00e2c\u00e1, S., Moore, B.M.: One-path reachability logic. In: LICS 2013, pp. 358\u2013367 (2013)","DOI":"10.1109\/LICS.2013.42"},{"key":"6_CR43","doi-asserted-by":"publisher","unstructured":"Rustan, K., Leino, M.: Verification of Object-Oriented Software. The KeY Approach, Lecture Notes in Computer Science (LNCS), vol.\u00a04334. Springer, Cham (2007). https:\/\/doi.org\/10.1007\/978-3-642-31762-0","DOI":"10.1007\/978-3-642-31762-0"},{"key":"6_CR44","doi-asserted-by":"publisher","unstructured":"Schneider, K., Brandt, J.: Quartz: a synchronous language for model-based design of reactive embedded systems. In: Ha, S., Teich, J. (eds.) Handbook of Hardware\/Software Codesign, pp. 1\u201330. Springer, Dordrecht (2017). https:\/\/doi.org\/10.1007\/978-94-017-7267-9_3","DOI":"10.1007\/978-94-017-7267-9_3"},{"key":"6_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-319-08918-8_29","volume-title":"Rewriting and Typed Lambda Calculi","author":"A \u015etef\u0103nescu","year":"2014","unstructured":"\u015etef\u0103nescu, A., Ciob\u00e2c\u0103, \u015e, Mereuta, R., Moore, B.M., \u015eerb\u0103nut\u0103, T.F., Ro\u015fu, G.: All-path reachability logic. In: Dowek, G. (ed.) RTA 2014. LNCS, vol. 8560, pp. 425\u2013440. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_29"},{"issue":"1","key":"6_CR46","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C Stirling","year":"1991","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89(1), 161\u2013177 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"6_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-031-51777-8_5","volume-title":"Dynamic Logic. New Trends and Applications - DaL\u00ed 2023","author":"T Takagi","year":"2024","unstructured":"Takagi, T., Do, C.M., Ogata, K.: Automated quantum program verification in dynamic quantum logic. In: Gierasimczuk, N., Vel\u00e1zquez-Quesada, F.R. (eds.) DaL\u00ed 2023. LNCS, vol. 14401, pp. 68\u201384. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-51777-8_5"},{"issue":"3","key":"6_CR48","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/s10817-019-09532-0","volume":"64","author":"G Tellez","year":"2020","unstructured":"Tellez, G., Brotherston, J.: Automatically verifying temporal properties of pointer programs with cyclic proof. J. Autom. Reason. 64(3), 555\u2013578 (2020)","journal-title":"J. Autom. Reason."},{"key":"6_CR49","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Mallet, F., Liu, Z.: A dynamic logic for verification of synchronous models based on theorem proving. Front. Comput. Sci. 16(4) (2022)","DOI":"10.1007\/s11704-022-1374-4"},{"key":"6_CR50","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102591","volume":"203","author":"Y Zhang","year":"2021","unstructured":"Zhang, Y., Wu, H., Chen, Y., Mallet, F.: A clock-based dynamic logic for the verification of CCSL specifications in synchronous systems. Sci. Comput. Program. 203, 102591 (2021)","journal-title":"Sci. Comput. Program."},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"Zilberstein, N., Dreyer, D., Silva, A.: Outcome logic: a unifying foundation for correctness and incorrectness reasoning. Proc. ACM Program. Lang. 7(OOPSLA1) (2023)","DOI":"10.1145\/3586045"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-7826-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T22:38:39Z","timestamp":1777847919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-7826-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9789819578252","9789819578269"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-7826-9_6","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":"1 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.setta2025.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}