{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:55:06Z","timestamp":1782878106451,"version":"3.54.5"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","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-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_16","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:52:13Z","timestamp":1776289933000},"page":"315-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5987-1080","authenticated-orcid":false,"given":"Kilian","family":"Lichtner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-2149","authenticated-orcid":false,"given":"Pascal","family":"Bergstr\u00e4\u00dfer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0775-7781","authenticated-orcid":false,"given":"Moses","family":"Ganardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4715-5096","authenticated-orcid":false,"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6421-4388","authenticated-orcid":false,"given":"Georg","family":"Zetzsche","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Archibald, J.K., Baer, J.: Cache coherence protocols: Evaluation using a multiprocessor simulation model. ACM Trans. Comput. Syst. 4(4), 273\u2013298 (1986). https:\/\/doi.org\/10.1145\/6513.6514","DOI":"10.1145\/6513.6514"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J.: Faster acceleration of counter automata in practice. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a02988, pp. 576\u2013590. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_42","DOI":"10.1007\/978-3-540-24730-2_42"},{"key":"16_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.7. Tech. rep., Department of Computer Science, The University of Iowa (2025), available at www.SMT-LIB.org"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Bergstr\u00e4\u00dfer, P., Ganardi, M., Lin, A.W., Zetzsche, G.: Ramsey quantifiers over automatic structures: Complexity and applications to verification. In: Baier, C., Fisman, D. (eds.) LICS \u201922: 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022. pp. 28:1\u201328:14. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533346","DOI":"10.1145\/3531130.3533346"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Bergstr\u00e4\u00dfer, P., Ganardi, M., Lin, A.W., Zetzsche, G.: Ramsey quantifiers in linear arithmetics. Proc. ACM Program. Lang. 8(POPL), 1\u201332 (2024). https:\/\/doi.org\/10.1145\/3632843","DOI":"10.1145\/3632843"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., McMillan, K.L., Rybalchenko, A.: Program verification as satisfiability modulo theories. In: Fontaine, P., Goel, A. (eds.) 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012. EPiC Series in Computing, vol.\u00a020, pp. 3\u201311. EasyChair (2012). https:\/\/doi.org\/10.29007\/1L7F","DOI":"10.29007\/1L7F"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011). https:\/\/doi.org\/10.1145\/1995376.1995394","DOI":"10.1145\/1995376.1995394"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), \u00a0569 (1965). https:\/\/doi.org\/10.1145\/365559.365617","DOI":"10.1145\/365559.365617"},{"key":"16_CR9","unstructured":"Gario, M., Micheli, A.: Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms. In: SMT Workshop 2015 (2015)"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Ginsburg, S., Spanier, E.: Semigroups, presburger formulas, and languages. Pacific journal of mathematics 16(2), 285\u2013296 (1966). https:\/\/doi.org\/10.2140\/pjm.1966.16.285","DOI":"10.2140\/pjm.1966.16.285"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 405\u2013416. PLDI \u201912, Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Leroux, J., Point, G.: Tapas: The talence presburger arithmetic suite. In: Kowalewski, S., Philippou, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05505, pp. 182\u2013185. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_18","DOI":"10.1007\/978-3-642-00768-2_18"},{"key":"16_CR13","doi-asserted-by":"publisher","unstructured":"Lichtner, K., Bergstr\u00e4\u00dfer, P., Ganardi, M., Lin, A.W., Zetzsche, G.: Fast ramsey quantifier elimination in LIRA (with applications to liveness checking). CoRR abs\/2511.05323 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2511.05323","DOI":"10.48550\/ARXIV.2511.05323"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Lichtner, K., Bergstr\u00e4\u00dfer, P., Ganardi, M., Lin, A.W., Zetzsche, G.: TACAS2026 AE Artifacts for \u201cFast Ramsey Quantifier Elimination in LIRA\u201d (2026). https:\/\/doi.org\/10.5281\/zenodo.18311746","DOI":"10.5281\/zenodo.18311746"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Manna, Z., Pnueli, A.: Formalization of properties of functional programs. J. ACM 17(3), 555\u2013569 (1970). https:\/\/doi.org\/10.1145\/321592.321606","DOI":"10.1145\/321592.321606"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"To, A.W., Libkin, L.: Recurrent reachability analysis in regular model checking. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a05330, pp. 198\u2013213. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_15","DOI":"10.1007\/978-3-540-89439-1_15"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"To, A.W., Libkin, L.: Algorithmic metatheorems for decidable LTL model checking over infinite systems. In: Ong, C.L. (ed.) Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06014, pp. 221\u2013236. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12032-9_16","DOI":"10.1007\/978-3-642-12032-9_16"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Veanes, M., Bj\u00f8rner, N.S., Nachmanson, L., Bereg, S.: Monadic decomposition. J. ACM 64(2), 14:1\u201314:28 (2017). https:\/\/doi.org\/10.1145\/3040488","DOI":"10.1145\/3040488"}],"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-032-22752-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:00:08Z","timestamp":1782874808000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_16","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":"16 April 2026","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":"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":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}