{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:35Z","timestamp":1776333455561,"version":"3.51.2"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227737","type":"print"},{"value":"9783032227744","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-3-032-22774-4_19","type":"book-chapter","created":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:17:42Z","timestamp":1776331062000},"page":"371-391","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstract Symbolic Finite Automata for Algorithmic Game Semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-2631","authenticated-orcid":false,"given":"Aleksandar S.","family":"Dimovski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,17]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. Electr. Notes Theor. Comput. Sci. 3, 2\u201314 (1996). https:\/\/doi.org\/10.1016\/S1571-0661(05)80398-6","DOI":"10.1016\/S1571-0661(05)80398-6"},{"key":"19_CR2","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994). https:\/\/doi.org\/10.1145\/186025.186051, http:\/\/doi.acm.org\/10.1145\/186025.186051","DOI":"10.1145\/186025.186051"},{"key":"19_CR4","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conf. Record of the Fourth ACM Symposium on POPL. pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973, http:\/\/doi.acm.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"19_CR5","doi-asserted-by":"publisher","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253\u2013291 (1997). https:\/\/doi.org\/10.1145\/244795.244800, http:\/\/doi.acm.org\/10.1145\/244795.244800","DOI":"10.1145\/244795.244800"},{"key":"19_CR6","doi-asserted-by":"publisher","unstructured":"D\u2019Antoni, L., Veanes, M.: Minimization of symbolic automata. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914. pp. 541\u2013554. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535849, https:\/\/doi.org\/10.1145\/2535838.2535849","DOI":"10.1145\/2535838.2535849"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364\u2013379 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.01.016","DOI":"10.1016\/j.tcs.2014.01.016"},{"key":"19_CR8","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Verifying annotated program families using symbolic game semantics. Theor. Comput. Sci. 706, 35\u201353 (2018). https:\/\/doi.org\/10.1016\/j.tcs.2017.09.029","DOI":"10.1016\/j.tcs.2017.09.029"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Fault localization by abstract interpretation and its applications. J. Comput. Lang. 80, 101288 (2024). https:\/\/doi.org\/10.1016\/J.COLA.2024.101288, https:\/\/doi.org\/10.1016\/j.cola.2024.101288","DOI":"10.1016\/J.COLA.2024.101288"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Imperative program synthesis by abstract static analysis and SMT mutations. In: Proceedings of the 24th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2025. pp. 27\u201340. ACM (2025). https:\/\/doi.org\/10.1145\/3742876.3742884, https:\/\/doi.org\/10.1145\/3742876.3742884","DOI":"10.1145\/3742876.3742884"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: On synthesizing presence conditions in numerical software product lines. In: Proceedings of the 29th ACM International Systems and Software Product Line Conference - Volume A, SPLC 2025. pp. 161\u2013171. ACM (2025). https:\/\/doi.org\/10.1145\/3744915.3748474, https:\/\/doi.org\/10.1145\/3744915.3748474","DOI":"10.1145\/3744915.3748474"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S.: Weakest safe context synthesis by symbolic game semantics and logical abduction. In: Proceedings of the 40th ACM\/SIGAPP Symposium on Applied Computing, SAC 2025. pp. 1990\u20131997. ACM (2025). https:\/\/doi.org\/10.1145\/3672608.3707849, https:\/\/doi.org\/10.1145\/3672608.3707849","DOI":"10.1145\/3672608.3707849"},{"key":"19_CR13","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Apel, S.: Lifted static analysis of dynamic program families by abstract interpretation. In: 35th European Conference on Object-Oriented Programming, ECOOP 2021. LIPIcs, vol.\u00a0194, pp. 14:1\u201314:28. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.14, https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2021.14","DOI":"10.4230\/LIPIcs.ECOOP.2021.14"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: A decision tree lifted domain for analyzing program families with numerical features. In: Fundamental Approaches to Software Engineering - 24th International Conference, FASE 2021, Proceedings. LNCS, vol. 12649, pp. 67\u201386. Springer (2021), https:\/\/arxiv.org\/abs\/2012.05863","DOI":"10.1007\/978-3-030-71500-7_4"},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: Program sketching using lifted analysis for numerical program families. In: NASA Formal Methods - 13th International Symposium, NFM 2021, Proceedings. LNCS, vol. 12673, pp. 95\u2013112. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_7, https:\/\/doi.org\/10.1007\/978-3-030-76384-8_7","DOI":"10.1007\/978-3-030-76384-8_7"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Brabrand, C., Wasowski, A.: Finding suitable variability abstractions for family-based analysis. In: FM 2016: Formal Methods - 21st International Symposium, Proceedings. LNCS, vol.\u00a09995, pp. 217\u2013234. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_14, https:\/\/doi.org\/10.1007\/978-3-319-48989-6_14","DOI":"10.1007\/978-3-319-48989-6_14"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Ghica, D.R., Lazic, R.: A counterexample-guided refinement tool for open procedural programs. In: Model Checking Software, 13th International SPIN Workshop, 2006, Proceedings. LNCS, vol.\u00a03925, pp. 288\u2013292. Springer (2006). https:\/\/doi.org\/10.1007\/11691617_17, https:\/\/doi.org\/10.1007\/11691617_17","DOI":"10.1007\/11691617_17"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Dimovski, A.S., Lazic, R.: Compositional software verification based on game semantics and process algebra. Int. J. Softw. Tools Technol. Transf. 9(1), 37\u201351 (2007). https:\/\/doi.org\/10.1007\/S10009-006-0005-Y, https:\/\/doi.org\/10.1007\/s10009-006-0005-y","DOI":"10.1007\/S10009-006-0005-Y"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., McCusker, G.: The regular-language semantics of second-order idealized algol. Theor. Comput. Sci. 309(1-3), 469\u2013502 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(03)00315-3","DOI":"10.1016\/S0304-3975(03)00315-3"},{"key":"19_CR20","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Murawski, A.S.: Compositional model extraction for higher-order concurrent programs. In: 12th International Conference TACAS 2006. LNCS, vol.\u00a03920, pp. 303\u2013317. Springer (2006). https:\/\/doi.org\/10.1007\/11691372_20, http:\/\/dx.doi.org\/10.1007\/11691372_20","DOI":"10.1007\/11691372_20"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Ghica, D.R., Tzevelekos, N.: A system-level game semantics. In: Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012. Electronic Notes in Theoretical Computer Science, vol.\u00a0286, pp. 191\u2013211. Elsevier (2012). https:\/\/doi.org\/10.1016\/j.entcs.2012.08.013, https:\/\/doi.org\/10.1016\/j.entcs.2012.08.013","DOI":"10.1016\/j.entcs.2012.08.013"},{"key":"19_CR22","doi-asserted-by":"publisher","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361\u2013416 (2000). https:\/\/doi.org\/10.1145\/333979.333989, https:\/\/doi.org\/10.1145\/333979.333989","DOI":"10.1145\/333979.333989"},{"key":"19_CR23","doi-asserted-by":"publisher","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Computer Aided Verification, 9th International Conference, CAV \u201997, Proceedings. LNCS, vol.\u00a01254, pp. 72\u201383. Springer (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10, https:\/\/doi.org\/10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"19_CR24","doi-asserted-by":"publisher","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Algorithmic probabilistic game semantics - playing games with automata. Formal Methods in System Design 43(2), 285\u2013312 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0173-1","DOI":"10.1007\/s10703-012-0173-1"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Koutavas, V., Lin, Y., Tzevelekos, N.: From bounded checking to verification of equivalence via symbolic up-to techniques. In: 28th International Conference, TACAS 2022. LNCS, vol. 13244, pp. 178\u2013195. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_10, https:\/\/doi.org\/10.1007\/978-3-030-99527-0_10","DOI":"10.1007\/978-3-030-99527-0_10"},{"key":"19_CR26","doi-asserted-by":"publisher","unstructured":"Laird, J.: A fully abstract trace semantics for general references. In: Automata, Languages and Programming, 34th International Colloquium, ICALP 2007, Proceedings. LNCS, vol.\u00a04596, pp. 667\u2013679. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73420-8_58, https:\/\/doi.org\/10.1007\/978-3-540-73420-8_58","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"19_CR27","doi-asserted-by":"publisher","unstructured":"Lin, Y., Tzevelekos, N.: Symbolic execution game semantics. In: 5th International Conference on FSCD 2020. LIPIcs, vol.\u00a0167, pp. 27:1\u201327:24. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.27, https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.27","DOI":"10.4230\/LIPIcs.FSCD.2020.27"},{"key":"19_CR28","doi-asserted-by":"publisher","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6(1), 11\u201344 (1995). https:\/\/doi.org\/10.1007\/BF01384313, http:\/\/dx.doi.org\/10.1007\/BF01384313","DOI":"10.1007\/BF01384313"},{"key":"19_CR29","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages 4(3-4), 120\u2013372 (2017). https:\/\/doi.org\/10.1561\/2500000034, https:\/\/doi.org\/10.1561\/2500000034","DOI":"10.1561\/2500000034"},{"key":"19_CR30","doi-asserted-by":"publisher","unstructured":"Murawski, A.S.: Reachability games and game semantics: Comparing nondeterministic programs. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008. pp. 353\u2013363. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/LICS.2008.24, http:\/\/dx.doi.org\/10.1109\/LICS.2008.24","DOI":"10.1109\/LICS.2008.24"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Murawski, A.S., Walukiewicz, I.: Third-order idealized algol with iteration is decidable. In: 8th International Conference, FOSSACS 2005. LNCS, vol.\u00a03441, pp. 202\u2013218. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-31982-5_13, http:\/\/dx.doi.org\/10.1007\/978-3-540-31982-5_13","DOI":"10.1007\/978-3-540-31982-5_13"},{"key":"19_CR32","doi-asserted-by":"publisher","unstructured":"Preda, M.D., Giacobazzi, R., Lakhotia, A., Mastroeni, I.: Abstract symbolic automata: Mixed syntactic\/semantic similarity analysis of executables. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium POPL 2015. pp. 329\u2013341. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676986, https:\/\/doi.org\/10.1145\/2676726.2676986","DOI":"10.1145\/2676726.2676986"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22774-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:17:46Z","timestamp":1776331066000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22774-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227737","9783032227744"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22774-4_19","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":"17 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}