{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:17Z","timestamp":1784793797168,"version":"3.55.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present , a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems.  implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems.  supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the  tool, and our own bespoke input. We present a mature version of  with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that  outperforms its only competitor in this domain.<\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_18","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:35Z","timestamp":1784791055000},"page":"340-353","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["sweap: Reactive Synthesis for\u00a0Infinite-State Integer Problems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2165-3698","authenticated-orcid":false,"given":"Shaun","family":"Azzopardi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-3151","authenticated-orcid":false,"given":"Luca","family":"Di Stefano","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8242-5357","authenticated-orcid":false,"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Di\u00a0Stefano, L., Piterman, N.: Code and benchmark data for \u201csweap: reactive synthesis for infinite-state integer problems\u201d (2026). https:\/\/doi.org\/10.5281\/zenodo.19684663","DOI":"10.5281\/zenodo.19684663"},{"key":"18_CR2","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Di\u00a0Stefano, L., Piterman, N.: Sweap: reactive synthesis for infinite-state integer problems (extended version) (2026). https:\/\/doi.org\/10.48550\/arXiv.2605.11992","DOI":"10.48550\/arXiv.2605.11992"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Di Stefano, L., Piterman, N., Schneider, G.: Full LTL synthesis over infinite-state arenas. In: Piskac, R., Rakamaric, Z. (eds.) 37th International Conference on Computer Aided Verification (CAV). LNCS, vol. 15934, pp. 274\u2013297. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_13","DOI":"10.1007\/978-3-031-98685-7_13"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Piterman, N., Schneider, G., Stefano, L.D.: LTL synthesis on infinite-state arenas defined by programs (2023). https:\/\/doi.org\/10.48550\/ARXIV.2307.09776, https:\/\/doi.org\/10.48550\/arXiv.2307.09776","DOI":"10.48550\/ARXIV.2307.09776"},{"issue":"5","key":"18_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? CoRR abs\/2206.11366 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2206.11366, https:\/\/doi.org\/10.48550\/arXiv.2206.11366","DOI":"10.48550\/ARXIV.2206.11366"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-030-25540-4_35","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: Temporal stream logic: synthesis beyond the bools. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 609\u2013629. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_35"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Solving infinite-state games via acceleration. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632899","DOI":"10.1145\/3632899"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Issy: a comprehensive tool for specification and synthesis of infinite-state reactive systems. In: Piskac, R., Rakamaric, Z. (eds.) 37th International Conference on Computer Aided Verification (CAV). LNCS, vol. 15934, pp. 298\u2013312. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_14","DOI":"10.1007\/978-3-031-98685-7_14"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Modular attractor acceleration in infinite-state games. In: Junges, S., Katz, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS. LNCS, vol. 16505, pp. 398\u2013418. Springer, Cham (2026). https:\/\/doi.org\/10.1007\/978-3-032-22752-2_21","DOI":"10.1007\/978-3-032-22752-2_21"},{"key":"18_CR12","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, pp. 886\u2013902. LNCS, Springer, Cham (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_69","DOI":"10.1007\/3-540-45061-0_69"},{"key":"18_CR13","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: SemML: enhancing automata-theoretic LTL synthesis with machine learning. In: Gurfinkel, A., Heule, M. (eds.) 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 15696, pp. 233\u2013253. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90643-5_12","DOI":"10.1007\/978-3-031-90643-5_12"},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Maderbacher, B., Bloem, R.: Reactive synthesis modulo theories using abstraction refinement. In: 22nd Conference on Formal Methods in Computer-Aided Design, FMCAD 2022, pp. 315\u2013324. TU Wien Academic Press (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":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11817963_14","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2006","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123\u2013136. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_14"},{"key":"18_CR16","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":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-662-49674-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Neider","year":"2016","unstructured":"Neider, D., Topcu, U.: An automaton learning approach to solving safety games over infinite graphs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 204\u2013221. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_12"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, 11\u201313 January 1989, pp. 179\u2013190. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"18_CR19","unstructured":"Prokop, M., Meggendorfer, T., Kret\u00ednsk\u00fd, J.: Semml 2.0: synthesizing controllers from LTL. In: 38th International Conference on Computer Aided Verification, CAV (2026)"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Rodr\u00edguez, A., Gorostiaga, F., S\u00e1nchez, C.: Counter example guided reactive synthesis for LTL modulo theories. In: Proc. of the 37th Int\u2019l Conference on Computer Aided Verification (CAV\u201925), Part IV. LNCS, vol. 15934, pp. 224\u2013248. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-98685-7_11, https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-98685-7_11","DOI":"10.1007\/978-3-031-98685-7_11"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Schmuck, A.K., Heim, P., Dimitrova, R., Nayak, S.P.: Localized attractor computations for infinite-state games. In: Gurfinkel, A., Ganesh, V. (eds.) 36th International Conference on Computer Aided Verification (CAV). LNCS, vol. 14683, pp. 135\u2013158. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_7","DOI":"10.1007\/978-3-031-65633-0_7"}],"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-032-32519-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:37Z","timestamp":1784791057000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_18","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":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}