{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:20:14Z","timestamp":1784830814994,"version":"3.55.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986840","type":"print"},{"value":"9783031986857","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Reactive synthesis is the process of automatically generating a correct system from a given temporal specification. In this paper, we address the problem of reactive synthesis for LTL modulo theories (\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textrm{LTL}^{\\mathcal {T}}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mtext>LTL<\/mml:mtext>\n                            <mml:mi>T<\/mml:mi>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    ), which extends LTL with literals from a first-order theory\n                    <jats:italic>and allows relating the values of data across time<\/jats:italic>\n                    . This logic allows describing complex dynamics both for the system and for the environment\u2014such as a numeric variable increasing monotonically over time. The logic also allows defining relations (and not only assignment) between variables, enabling permissive shielding.\n                  <\/jats:p>\n                  <jats:p>\n                    We propose a sound algorithm called Counter-Example Guided Reactive Synthesis modulo theories (CEGRES), whose core is the novel concept of\n                    <jats:italic>reactive tautology<\/jats:italic>\n                    , which are valid temporal formulas that preserve the semantics of the specification but make the algorithm conclusive. Although realizability for full\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\textrm{LTL}^{\\mathcal {T}} $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mtext>LTL<\/mml:mtext>\n                            <mml:mi>T<\/mml:mi>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is undecidable in general, we prove that CEGRES is terminating for some important theories and for arbitrary theories when specifications do not fetch data across time. We include an empirical evaluation that shows that CEGRES can solve many reactive synthesis problems of practical interest.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_11","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:05Z","timestamp":1753155125000},"page":"224-248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Counter Example Guided Reactive Synthesis for\u00a0LTL Modulo Theories$$^*$$"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-3464-8667","authenticated-orcid":false,"given":"Andoni","family":"Rodr\u00edguez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3478-3408","authenticated-orcid":false,"given":"Felipe","family":"Gorostiaga","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3927-4773","authenticated-orcid":false,"given":"Cesar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. arXiv abs\/1708.08611 (2017). https:\/\/doi.org\/10.48550\/ARXIV.1708.08611","DOI":"10.48550\/ARXIV.1708.08611"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Piterman, N., Stefano, L.D., Schneider, G.: Symbolic infinite-state LTL synthesis (2024). https:\/\/doi.org\/10.48550\/arXiv.2307.09776","DOI":"10.48550\/arXiv.2307.09776"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Proceedings of the 21st International Conference in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). LNCS, vol.\u00a09035, pp. 533\u2013548. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer-Verlag (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8","DOI":"10.1007\/978-3-540-74113-8"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Brizzio, M., Gorostiaga, F., Sanchez, C., Degiovanni, R.: Mode-based reactive synthesis. In: Proceedings of the 17th NASA Formal Methods International Symposium (NFM 2025). LNCS (2025). https:\/\/doi.org\/10.1007\/978-3-031-60698-4_1","DOI":"10.1007\/978-3-031-60698-4_1"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10\\hat 20 $$states and beyond. In: Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS 1990), pp. 428\u2013439. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113767","DOI":"10.1109\/LICS.1990.113767"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Choi, W., Finkbeiner, B., Piskac, R., Santolucito, M.: Can reactive synthesis and syntax-guided synthesis be friends? In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022), pp. 229\u2013243. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523429","DOI":"10.1145\/3519939.3523429"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"11_CR9","first-page":"1759","volume":"4","author":"D Corsi","year":"2024","unstructured":"Corsi, D., Amir, G., Rodr\u00edguez, A., Katz, G., S\u00e1nchez, C., Fox, R.: Verification-guided shielding for deep reinforcement learning. RLJ 4, 1759\u20131780 (2024)","journal-title":"RLJ"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni, L., Veanes, M.: The power of symbolic automata and transducers. In: Proceedings of the 29th International Conference in Computer Aided Verification (CAV 2017), Part I. LNCS, vol. 10426, pp. 47\u201367. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_3","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B.: Synthesis of reactive systems. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a045, pp. 72\u201398. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Heim, P., Passing, N.: Temporal stream logic modulo theories. In: Proceedings of the 25th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2022). LNCS, vol. 13242, pp. 325\u2013346. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_17","DOI":"10.1007\/978-3-030-99253-8_17"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal stream logic: synthesis beyond the Bools. In: Proceedings of the 31st International Conference on Computer Aided Verification (CAV 2019), Part I. LNCS, vol. 11561, pp. 609\u2013629. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_35","DOI":"10.1007\/978-3-030-25540-4_35"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.D.: Towards realizability checking of contracts using theories. In: Proceedings of the 7th International Symposium NASA Formal Methods (NFM 2015). LNCS, vol.\u00a09058, pp. 173\u2013187. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13","DOI":"10.1007\/978-3-319-17524-9_13"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Geatti, L., Gianola, A., Gigante, N.: Linear temporal logic modulo theories over finite traces. In: Proceedings of the 31st International Joint Conference on Artificial Intelligence, (IJCAI 2022), pp. 2641\u20132647. ijcai.org (2022). https:\/\/doi.org\/10.24963\/ijcai.2022\/366","DOI":"10.24963\/ijcai.2022\/366"},{"key":"11_CR16","unstructured":"Geatti, L., Gianola, A., Gigante, N.: A general automata model for first-order temporal logics. arXive abs\/2405.20057 (2024)."},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Geatti, L., Gianola, A., Gigante, N., Winkler, S.: Decidable fragments of LTL$${_f}$$ modulo theories. In: Proceedings of the 26th European Conference on Artificial Intelligence (ECAI 2023). Frontiers in Artificial Intelligence and Applications, vol.\u00a0372, pp. 811\u2013818. IOS Press (2023). https:\/\/doi.org\/10.3233\/FAIA230348","DOI":"10.3233\/FAIA230348"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Solving infinite-state games via acceleration. Proc. ACM Program. Lang. 8(POPL), 1696\u20131726 (2024). https:\/\/doi.org\/10.1145\/3632899","DOI":"10.1145\/3632899"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Issy: A comprehensive tool for specification and synthesis of infinite-state reactive systems (2025). https:\/\/doi.org\/10.48550\/arXiv.2502.03013","DOI":"10.48550\/arXiv.2502.03013"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Translation of temporal logic for efficient infinite-state reactive synthesis. Proc. ACM Program. Lang. 9(POPL) (2025). https:\/\/doi.org\/10.1145\/3704888","DOI":"10.1145\/3704888"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Katis, A., Fedyukovich, G., Guo, H., Gacek, A., Backes, J., Gurfinkel, A., Whalen, M.W.: Validity-guided synthesis of reactive systems from assume-guarantee contracts. In: Proceedings of the 24th Int\u2019l Conference on Tools and Algorithms for the Construction and Analysis of Systems, (TACAS 2018), Part II. LNCS, vol. 10806, pp. 176\u2013193. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_10","DOI":"10.1007\/978-3-319-89963-3_10"},{"key":"11_CR22","unstructured":"Kim, K., et al.: Realizable continuous-space shields for safe reinforcement learning. In: Proceedings of the 7th Annual Learning for Dynamics & Control Conference (L4DC 2025). PMLR (2025). https:\/\/proceedings.mlr.press\/v242\/zhou24a.html"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M., Rieder, S.: Guessing winning policies in LTL synthesis by semantic learning. In: Proceedings of the 35th International Conference on Computer Aided Verification (CAV 2023). LNCS, vol. 13964, pp. 390\u2013414. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_20","DOI":"10.1007\/978-3-031-37706-8_20"},{"key":"11_CR24","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-031-90643-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J K\u0159et\u00ednsk\u00fd","year":"2025","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: SemML: enhancing automata-theoretic LTL synthesis with machine learning. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 233\u2013253. Springer Nature Switzerland, Cham (2025)"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: Proceedings of the 22nd International Conference on Formal Methods in Computer-Aided Design, (FMCAD 2022), pp. 315\u2013324. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_38","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_38"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Maderbacher, B., Windisch, F., Bloem, R.: Synthesis from infinite-state generalized reactivity(1) specifications. In: Proceedings of the 12th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation on Software Engineering Methodologies, (ISoLA 2024), Part IV. LNCS, vol. 15222, pp. 281\u2013301. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-75387-9_17","DOI":"10.1007\/978-3-031-75387-9_17"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing (PODC 1990), pp. 377\u2013410. ACM (1990). https:\/\/doi.org\/10.1145\/93385.93442","DOI":"10.1145\/93385.93442"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer (1995). https:\/\/doi.org\/10.1007\/978-1-4612-4222-2","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Eager abstraction for symbolic model checking. In: Proceedings of the 30th International Conference in Computer Aided Verification (CAV 2018), Part I. LNCS, vol. 10981, pp. 191\u2013208. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_11","DOI":"10.1007\/978-3-319-96145-3_11"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"11_CR31","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":"11_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (FOCS 1977), pp. 46\u201367. IEEE CS Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th Annual ACM Sympoisum on Principles of Programming Languages (POPL 1989), pp. 179\u2013190. ACM Press (1989)","DOI":"10.1145\/75277.75293"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652\u2013671. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035790"},{"key":"11_CR35","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., Amir, G., Corsi, D., S\u00e1nchez, C., Katz, G.: Shield synthesis for LTL modulo theories. In: Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI 2025), pp. 15134\u201315142. AAAI Press (2025). https:\/\/doi.org\/10.1609\/AAAI.V39I14.33660","DOI":"10.1609\/AAAI.V39I14.33660"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., Gorostiaga, F., S\u00e1nchez, C.: Predictable and performant reactive synthesis modulo theories via functional synthesis. In: Akshay, S., Niemetz, A., Sankaranarayanan, S. (eds.) Proceedings of 22nd the International Symposium on Automated Technology for Verification and Analysis (ATVA 2024). Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-78750-8_2","DOI":"10.1007\/978-3-031-78750-8_2"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Boolean abstractions for realizabilty modulo theories. In: Proceedings of the 35th International Conference on Computer Aided Verification (CAV 2023). LNCS, vol. 13966. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_15","DOI":"10.1007\/978-3-031-37709-9_15"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Adaptive reactive synthesis for LTL and LTLf modulo theories. In: Proceedings of the 38th AAAI Conference on Artificial Intelligence (AAAI 2024), pp. 10679\u201310686. AAAI Press (2024). https:\/\/doi.org\/10.1609\/AAAI.V38I9.28939","DOI":"10.1609\/AAAI.V38I9.28939"},{"key":"11_CR39","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2024.100971","volume":"140","author":"A Rodr\u00edguez","year":"2024","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Realizability modulo theories. J. Logical Algebraic Methods Program. 140, 100971 (2024). https:\/\/doi.org\/10.1016\/j.jlamp.2024.100971","journal-title":"J. Logical Algebraic Methods Program."},{"key":"11_CR40","doi-asserted-by":"publisher","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: GenSys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces. In: Proc. of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE 2021), pp. 1585\u20131589. ACM (2021). https:\/\/doi.org\/10.1145\/3468264.3473126","DOI":"10.1145\/3468264.3473126"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"Samuel, S., D\u2019Souza, D., Komondoor, R.: Symbolic fixpoint algorithms for logical LTL games. In: Proceedings of the 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2023), pp. 698\u2013709. IEEE (2023). https:\/\/doi.org\/10.1109\/ASE56229.2023.00212","DOI":"10.1109\/ASE56229.2023.00212"},{"key":"11_CR42","doi-asserted-by":"publisher","unstructured":"Schmuck, A., Heim, P., Dimitrova, R., Nayak, S.P.: Localized attractor computations for infinite-state games. In: Proceedings of the 36th Int\u2019l Conf. on Computer Aided Verification (CAV 2024), Part III. LNCS, vol. 14683, pp. 135\u2013158. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_7","DOI":"10.1007\/978-3-031-65633-0_7"},{"key":"11_CR43","doi-asserted-by":"publisher","unstructured":"Veanes, M., Ball, T., Ebner, G., Zhuchko, E.: Symbolic automata: $$\\omega $$-regularity modulo theories. Proc. ACM Program. Lang. 9(POPL) (2025). https:\/\/doi.org\/10.1145\/3704838","DOI":"10.1145\/3704838"},{"key":"11_CR44","doi-asserted-by":"publisher","unstructured":"Wu, M., Wang, J., Deshmukh, J., Wang, C.: Shield synthesis for real: enforcing safety in cyber-physical systems. In: Proceedings of 19th Formal Methods in Computer Aided Design, (FMCAD 2019), pp. 129\u2013137. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894264","DOI":"10.23919\/FMCAD.2019.8894264"}],"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-031-98685-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T07:40:05Z","timestamp":1784533205000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_11","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":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","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":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}