{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T20:47:44Z","timestamp":1775249264538,"version":"3.50.1"},"publisher-location":"Cham","reference-count":80,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656262","type":"print"},{"value":"9783031656279","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a new angle on solving quantified linear integer arithmetic based on combining the automata-based approach, where numbers are understood as bitvectors, with ideas from (nowadays prevalent) algebraic approaches, which work directly with numbers. This combination is enabled by a\u00a0fine-grained version of the duality between automata and arithmetic formulae. In particular, we employ a\u00a0construction where states of automaton are obtained as derivatives of arithmetic formulae: then every state corresponds to a\u00a0formula. Optimizations based on techniques and ideas transferred from the world of algebraic methods are used on thousands of automata states, which dramatically amplifies their effect. The merit of this combination of automata with algebraic methods is demonstrated by our prototype implementation being competitive to and even superior to state-of-the-art SMT solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_3","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"42-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Algebraic Reasoning Meets Automata in\u00a0Solving Linear Integer Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7982-0946","authenticated-orcid":false,"given":"Peter","family":"Habermehl","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4375-7954","authenticated-orcid":false,"given":"Vojt\u011bch","family":"Havlena","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2428-8547","authenticated-orcid":false,"given":"Michal","family":"He\u010dko","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"3_CR1","unstructured":"The Li\u00e8ge automata-based symbolic handler (Lash). https:\/\/people.montefiore.uliege.be\/boigelot\/research\/lash\/"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., et al.: Trau: SMT solver for string constraints. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 \u2013 November 2, 2018, pp.\u00a01\u20135. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602997","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theoret. Comput. Sci. 155(2), 291\u2013319 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00182-4, http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397595001824","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) ETAPS 2022, Part I. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"3_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"issue":"1","key":"3_CR6","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L Berman","year":"1980","unstructured":"Berman, L.: The complexity of logical theories. Theoret. Comput. Sci. 11(1), 71\u201377 (1980). https:\/\/doi.org\/10.1016\/0304-3975(80)90037-7","journal-title":"Theoret. Comput. Sci."},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1016\/j.tcs.2022.12.009","volume":"943","author":"M Berzish","year":"2023","unstructured":"Berzish, M., et al.: Towards more efficient methods for solving regular-expression heavy string constraints. Theor. Comput. Sci. 943, 50\u201372 (2023). https:\/\/doi.org\/10.1016\/j.tcs.2022.12.009","journal-title":"Theor. Comput. Sci."},{"key":"3_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-031-27481-7_23","volume-title":"FM 2023","author":"F Blahoudek","year":"2023","unstructured":"Blahoudek, F., et al.: Word equations in synergy with regular constraints. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 403\u2013423. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_23"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45744-5_50","volume-title":"Automated Reasoning","author":"B Boigelot","year":"2001","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 611\u2013625. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_50"},{"issue":"3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/1071596.1071601","volume":"6","author":"B Boigelot","year":"2005","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614\u2013633 (2005). https:\/\/doi.org\/10.1145\/1071596.1071601","journal-title":"ACM Trans. Comput. Log."},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/BFb0055049","volume-title":"Automata, Languages and Programming","author":"B Boigelot","year":"1998","unstructured":"Boigelot, B., Rassart, S., Wolper, P.: On the expressiveness of real and integer arithmetic automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 152\u2013163. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055049"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45619-8_1","volume-title":"Logic Programming","author":"B Boigelot","year":"2002","unstructured":"Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: an overview. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 1\u201320. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45619-8_1"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming \u2014 CAAP \u201996","author":"A Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 30\u201343. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61064-2_27"},{"key":"3_CR14","unstructured":"Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. In: Proceedings of the Symposium Mathematics Theory of Automata (New York, 1962), Microwave Research Institute Symposia Series, Brooklyn, NY, vol. XII, pp. 529\u2013561. Polytechnic (1963)"},{"issue":"4","key":"3_CR15","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964). https:\/\/doi.org\/10.1145\/321239.321249","journal-title":"J. ACM"},{"key":"3_CR16","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Method, and Philosophy of Science 1960. Stanford Univ. Press, Stanford (1962)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Zeitscrift fur mathematische Logic und Grundlagen der Mathematik 6, 66\u201392 (1960)","journal-title":"Zeitscrift fur mathematische Logic und Grundlagen der Mathematik"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Chen, T., et al.: Solving string constraints with regex-dependent functions through transducers with priorities and variables. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498707","DOI":"10.1145\/3498707"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Solving string constraints with lengths by stabilization. Proc. ACM Program. Lang. 7(OOPSLA2) (oct 2023). https:\/\/doi.org\/10.1145\/3622872","DOI":"10.1145\/3622872"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., Chocholat\u00fd, D., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., S\u00ed\u010d, J.: Z3-noodler: an automata-based string solver (technical report). CoRR abs\/2310.08327 (2023). https:\/\/doi.org\/10.48550\/arXiv.2310.08327","DOI":"10.48550\/arXiv.2310.08327"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Chocholat\u00fd, D., et al.: Mata: a fast and simple finite automata library (technical report). CoRR abs\/2310.10136 (2023). https:\/\/doi.org\/10.48550\/arXiv.2310.10136, To appear at TACAS\u201923","DOI":"10.48550\/arXiv.2310.10136"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/3-540-57163-9_13","volume-title":"Fundamentals of Computation Theory","author":"P Chrzastowski-Wachtel","year":"1993","unstructured":"Chrzastowski-Wachtel, P., Raczunas, M.: Liveness of weighted circuits and the diophantine problem of Frobenius. In: \u00c9sik, Z. (ed.) FCT 1993. LNCS, vol. 710, pp. 171\u2013180. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57163-9_13"},{"key":"3_CR23","first-page":"91","volume":"7","author":"D Cooper","year":"1972","unstructured":"Cooper, D.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91\u201399 (1972)","journal-title":"Mach. Intell."},{"key":"3_CR24","unstructured":"Cox, A., Leasure, J.: Model checking regular language constraints. CoRR abs\/1708.09073 (2017)"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Dantzig, G.B.: Inductive proof of the simplex method. IBM J. Res. Dev. 4(5), 505\u2013506 (1960). https:\/\/doi.org\/10.1147\/RD.45.0505","DOI":"10.1147\/RD.45.0505"},{"issue":"3","key":"3_CR26","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM"},{"issue":"6","key":"3_CR27","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T van Dijk","year":"2017","unstructured":"van Dijk, T., van de Pol, J.: SYLVAN: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675\u2013696 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0433-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-12002-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Doyen","year":"2010","unstructured":"Doyen, L., Raskin, J.-F.: Antichain algorithms for finite automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2\u201322. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_2"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-15375-4_26","volume-title":"CONCUR 2010 - Concurrency Theory","author":"A Durand-Gasselin","year":"2010","unstructured":"Durand-Gasselin, A., Habermehl, P.: On the use of non-deterministic automata for Presburger arithmetic. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 373\u2013387. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_26"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-58216-9_30","volume-title":"Logic Programming and Automated Reasoning","author":"U Egly","year":"1994","unstructured":"Egly, U.: On the value of antiprenexing. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 69\u201383. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58216-9_30"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"Computer Aided Verification","author":"J Elgaard","year":"1998","unstructured":"Elgaard, J., Klarlund, N., M\u00f8ller, A.: MONA 1.x: new techniques for WS1S and WS2S. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 516\u2013520. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028773"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-662-54577-5_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Fiedor","year":"2017","unstructured":"Fiedor, T., Hol\u00edk, L., Jank\u016f, P., Leng\u00e1l, O., Vojnar, T.: Lazy automata techniques for WS1S. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 407\u2013425. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_24"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-662-46681-0_59","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Fiedor","year":"2015","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Nested antichains for WS1S. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 658\u2013674. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_59"},{"issue":"3","key":"3_CR34","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s00236-018-0331-z","volume":"56","author":"T Fiedor","year":"2019","unstructured":"Fiedor, T., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Nested antichains for WS1S. Acta Informatica 56(3), 205\u2013228 (2019). https:\/\/doi.org\/10.1007\/s00236-018-0331-z","journal-title":"Acta Informatica"},{"key":"3_CR35","unstructured":"Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: Proceedings of the SIAM-AMS Symposium in Applied Mathematics, vol.\u00a07, pp. 27\u201441 (1974)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"issue":"3\u20134","key":"3_CR37","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/s10472-007-9078-x","volume":"50","author":"S Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50(3\u20134), 231\u2013254 (2007). https:\/\/doi.org\/10.1007\/s10472-007-9078-x","journal-title":"Ann. Math. Artif. Intell."},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-70844-5_17","volume-title":"Implementation and Applications of Automata","author":"R van Glabbeek","year":"2008","unstructured":"van Glabbeek, R., Ploeger, B.: Five determinisation algorithms. In: Ibarra, O.H., Ravikumar, B. (eds.) CIAA 2008. LNCS, vol. 5148, pp. 161\u2013170. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70844-5_17"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-63174-7_5","volume-title":"Automata Implementation","author":"J Glenn","year":"1997","unstructured":"Glenn, J., Gasarch, W.: Implementing WS1S via finite automata. In: Raymond, D., Wood, D., Yu, S. (eds.) WIA 1996. LNCS, vol. 1260, pp. 50\u201363. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63174-7_5"},{"key":"3_CR40","unstructured":"Google: RE2. https:\/\/github.com\/google\/re2"},{"issue":"3","key":"3_CR41","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/3242953.3242964","volume":"5","author":"C Haase","year":"2018","unstructured":"Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News 5(3), 67\u201382 (2018). https:\/\/doi.org\/10.1145\/3242953.3242964","journal-title":"ACM SIGLOG News"},{"key":"3_CR42","doi-asserted-by":"publisher","unstructured":"Habermehl, P., Havlena, V., Hol\u00edk, L., He\u010dko, M., Leng\u00e1l, O.: Algebraic reasoning meets automata in solving linear integer arithmetic (technical report). CoRR abs\/2403.18995 (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.18995","DOI":"10.48550\/arXiv.2403.18995"},{"key":"3_CR43","doi-asserted-by":"publisher","unstructured":"Habermehl, P., Havlena, V., Hol\u00edk, L., He\u010dko, M., Leng\u00e1l, O.: Artifact for the cav\u201924 paper \u201cAlgebraic reasoning meets automata in solving linear integer arithmetic\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.10996343","DOI":"10.5281\/zenodo.10996343"},{"key":"3_CR44","doi-asserted-by":"publisher","unstructured":"Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., Vales, O., Vojnar, T.: Antiprenexing for WSkS: a little goes a long way. In: Albert, E., Kov\u00e1cs, L. (eds.) LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22\u201327, 2020. EPiC Series in Computing, vol.\u00a073, pp. 298\u2013316. EasyChair (2020). https:\/\/doi.org\/10.29007\/6bfc","DOI":"10.29007\/6bfc"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-29436-6_18","volume-title":"Automated Deduction \u2013 CADE 27","author":"V Havlena","year":"2019","unstructured":"Havlena, V., Hol\u00edk, L., Leng\u00e1l, O., Vojnar, T.: Automata terms in a lazy WSkS decision procedure. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 300\u2013318. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_18"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JG Henriksen","year":"1995","unstructured":"Henriksen, J.G., et al.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89\u2013110. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60630-0_5"},{"key":"3_CR48","unstructured":"He\u010dko, M.: Amaya (2024). https:\/\/github.com\/MichalHe\/amaya"},{"key":"3_CR49","doi-asserted-by":"publisher","unstructured":"Hieronymi, P., Ma, D., Oei, R., Schaeffer, L., Schulz, C., Shallit, J.O.: Decidability for Sturmian words. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, G\u00f6ttingen, Germany (Virtual Conference). LIPIcs, vol.\u00a0216, pp. 24:1\u201324:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2022.24","DOI":"10.4230\/LIPICS.CSL.2022.24"},{"key":"3_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-030-34175-6_24","volume-title":"Programming Languages and Systems","author":"L Hol\u00edk","year":"2019","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Saarikivi, O., Turo\u0148ov\u00e1, L., Veanes, M., Vojnar, T.: Succinct determinisation of counting automata via sphere construction. In: Lin, A.W. (ed.) APLAS 2019. LNCS, vol. 11893, pp. 468\u2013489. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34175-6_24"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Hopcroft, J.: An $$n$$ log $$n$$ algorithm for minimizing states in a finite automaton. In: Theory of Machines and Computations (Proc. Internat. Sympos., Technion, Haifa, 1971), pp. 189\u2013196. Academic Press, New York-London (1971)","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"3_CR52","doi-asserted-by":"publisher","unstructured":"Hu, D., Wu, Z.: String constraints with regex-counting and string-length solved more efficiently. In: Hermanns, H., Sun, J., Bu, L. (eds.) SETTA 2023. LNCS, vol. 14464, pp. 1\u201320. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-981-99-8664-4_1","DOI":"10.1007\/978-981-99-8664-4_1"},{"key":"3_CR53","unstructured":"Hyperscan.io (2021). https:\/\/www.hyperscan.io\/"},{"key":"3_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-030-25543-5_4","volume-title":"Computer Aided Verification","author":"M Jon\u00e1\u0161","year":"2019","unstructured":"Jon\u00e1\u0161, M., Strej\u010dek, J.: Q3B: an efficient BDD-based SMT solver for quantified bit-vectors. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 64\u201373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_4"},{"issue":"2","key":"3_CR55","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/1342991.1342995","volume":"9","author":"F Klaedtke","year":"2008","unstructured":"Klaedtke, F.: Bounds on the automata size for presburger arithmetic. ACM Trans. Comput. Log. 9(2), 11:1-11:34 (2008). https:\/\/doi.org\/10.1145\/1342991.1342995","journal-title":"ACM Trans. Comput. Log."},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/3-540-48683-6_35","volume-title":"Computer Aided Verification","author":"N Klarlund","year":"1999","unstructured":"Klarlund, N.: A theory of restrictions for logics and automata. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 406\u2013417. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_35"},{"issue":"4","key":"3_CR57","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1142\/S012905410200128X","volume":"13","author":"N Klarlund","year":"2002","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: Mona implementation secrets. Int. J. Found. Comput. Sci. 13(4), 571\u2013586 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"3_CR58","doi-asserted-by":"publisher","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-50497-0","DOI":"10.1007\/978-3-662-50497-0"},{"issue":"2","key":"3_CR59","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/2076450.2076472","volume":"55","author":"V Kuncak","year":"2012","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. Commun. ACM 55(2), 103\u2013111 (2012). https:\/\/doi.org\/10.1145\/2076450.2076472","journal-title":"Commun. ACM"},{"key":"3_CR60","doi-asserted-by":"publisher","unstructured":"Kuper, G.M., Libkin, L., Paredaens, J. (eds.): Constraint Databases. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-662-04031-7","DOI":"10.1007\/978-3-662-04031-7"},{"key":"3_CR61","doi-asserted-by":"publisher","unstructured":"Monniaux, D.: Automatic modular abstractions for linear constraints. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009. pp. 140\u2013151. ACM (2009). https:\/\/doi.org\/10.1145\/1480881.1480899","DOI":"10.1145\/1480881.1480899"},{"key":"3_CR62","doi-asserted-by":"publisher","unstructured":"Moseley, D., et al.: Derivative based nonbacktracking real-world regex matching with backtracking semantics. Proc. ACM Program. Lang. 7(PLDI), 1026\u20131049 (2023). https:\/\/doi.org\/10.1145\/3591262","DOI":"10.1145\/3591262"},{"key":"3_CR63","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":"3_CR64","unstructured":"Presburger, M.: \u00dcber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Comptes Rendus du I congr\u00e8s de Math\u00e9maticiens des Pays Slaves, pp. 92\u2014101 (1929)"},{"key":"3_CR65","doi-asserted-by":"publisher","unstructured":"Pugh, W.W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Martin, J.L. (ed.) Proceedings Supercomputing \u201991, Albuquerque, NM, USA, November 18\u201322, 1991, pp. 4\u201313. ACM (1991). https:\/\/doi.org\/10.1145\/125826.125848","DOI":"10.1145\/125826.125848"},{"issue":"3","key":"3_CR66","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Formal Methods Syst. Des. 51(3), 500\u2013532 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0290-y","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"3_CR67","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/S10703-017-0270-2","volume":"55","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Kuncak, V., Tinelli, C., Barrett, C.W., Deters, M.: Refutation-based synthesis in SMT. Formal Methods Syst. Des. 55(2), 73\u2013102 (2019). https:\/\/doi.org\/10.1007\/S10703-017-0270-2","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR68","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de\u00a0Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design. FMCAD \u201914, Austin, Texas, pp. 195-202. FMCAD Inc. (2014)","DOI":"10.1109\/FMCAD.2014.6987613"},{"key":"3_CR69","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001). https:\/\/www.sciencedirect.com\/book\/9780444508133\/handbook-of-automated-reasoning"},{"key":"3_CR70","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"key":"3_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-540-70889-6_5","volume-title":"Hardware and Software, Verification and Testing","author":"T Schuele","year":"2007","unstructured":"Schuele, T., Schneider, K.: Verification of data paths using unbounded integers: automata strike back. In: Bin, E., Ziv, A., Ur, S. (eds.) HVC 2006. LNCS, vol. 4383, pp. 65\u201380. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70889-6_5"},{"key":"3_CR72","unstructured":"SMT-LIB: LIA (2023). https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMT-LIB-benchmarks\/LIA"},{"key":"3_CR73","unstructured":"SMT-LIB: NIA (2023). https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMT-LIB-benchmarks\/NIA"},{"key":"3_CR74","doi-asserted-by":"publisher","unstructured":"Stanford, C., Veanes, M., Bj\u00f8rner, N.: Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI 2021, New York, NY, USA, pp. 620\u2013635. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3453483.3454066","DOI":"10.1145\/3453483.3454066"},{"key":"3_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11691617_18","volume-title":"Model Checking Software","author":"C Topnik","year":"2006","unstructured":"Topnik, C., Wilhelm, E., Margaria, T., Steffen, B.: jMosel: a stand-alone tool and jABC plugin for M2L(Str). In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 293\u2013298. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691617_18"},{"key":"3_CR76","doi-asserted-by":"publisher","unstructured":"Traytel, D.: A coalgebraic decision procedure for WS1S. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany. LIPIcs, vol.\u00a041, pp. 487\u2013503. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2015.487","DOI":"10.4230\/LIPIcs.CSL.2015.487"},{"key":"3_CR77","doi-asserted-by":"publisher","unstructured":"Traytel, D., Nipkow, T.: Verified decision procedures for MSO on words based on derivatives of regular expressions. J. Funct. Program. 25 (2015). https:\/\/doi.org\/10.1017\/S0956796815000246","DOI":"10.1017\/S0956796815000246"},{"key":"3_CR78","doi-asserted-by":"publisher","unstructured":"Turonov\u00e1, L., Hol\u00edk, L., Leng\u00e1l, O., Saarikivi, O., Veanes, M., Vojnar, T.: Regex matching with counting-set automata. Proc. ACM Program. Lang. 4(OOPSLA), 218:1\u2013218:30 (2020). https:\/\/doi.org\/10.1145\/3428286","DOI":"10.1145\/3428286"},{"key":"3_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-60360-3_30","volume-title":"Static Analysis","author":"P Wolper","year":"1995","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 21\u201332. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60360-3_30"},{"key":"3_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 1\u201319. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_1"}],"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-65627-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:54Z","timestamp":1721934114000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":80,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}