{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:07Z","timestamp":1747593607087,"version":"3.40.5"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"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,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"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>\n          <jats:p>SMT solvers use sophisticated techniques for polynomial (linear or non-linear) integer arithmetic. In contrast, non-polynomial integer arithmetic has mostly been neglected so far. However, in the context of program verification, polynomials are often insufficient to capture the behavior of the analyzed system without resorting to approximations. In the last years, <jats:italic>incremental linearization<\/jats:italic> has been applied successfully to satisfiability modulo real arithmetic with transcendental functions. We adapt this approach to an extension of polynomial integer arithmetic with exponential functions. Here, the key challenge is to compute suitable <jats:italic>lemmas<\/jats:italic> that eliminate the current model from the search space if it violates the semantics of exponentiation. An empirical evaluation of our implementation shows that our approach is highly effective in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_21","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"344-365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Satisfiability Modulo Exponential Integer Arithmetic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0902-1994","authenticated-orcid":false,"given":"Florian","family":"Frohn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010). https:\/\/doi.org\/10.1007\/S10817-009-9149-2","DOI":"10.1007\/S10817-009-9149-2"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: CVC5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401\u2013424 (2008). https:\/\/doi.org\/10.1007\/s10009-008-0064-3","DOI":"10.1007\/s10009-008-0064-3"},{"key":"21_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). (2016). https:\/\/smt-lib.org\/"},{"key":"21_CR5","doi-asserted-by":"publisher","unstructured":"Benedikt, M., Chistikov, D., Mansutti, A.: The complexity of Presburger arithmetic with power or powers. In: Etessami, K., Feige, U., Puppis, G. (eds.) ICALP 2023. LIPIcs, vol. 261, pp. 112:1\u2013112:18 (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2023.112","DOI":"10.4230\/LIPIcs.ICALP.2023.112"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-14295-6_23","volume-title":"Computer Aided Verification","author":"M Bozga","year":"2010","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 227\u2013242. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23"},{"key":"21_CR7","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Relational analysis of integer programs. Technical report, TR-2012-10, VERIMAG (2012). https:\/\/www-verimag.imag.fr\/TR\/TR-2012-10.pdf"},{"key":"21_CR8","unstructured":"CHC Competition. https:\/\/chc-comp.github.io"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-94144-8_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Cimatti","year":"2018","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 383\u2013398. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_23"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1\u201319:52 (2018). https:\/\/doi.org\/10.1145\/3230639","DOI":"10.1145\/3230639"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Lipparini, E., Sebastiani, R.: Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) ATVA\u00a02022. LNCS, vol. 13505, pp. 137\u2013153. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_9","DOI":"10.1007\/978-3-031-19992-9_9"},{"key":"21_CR13","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"},{"issue":"3\u20134","key":"21_CR14","doi-asserted-by":"publisher","first-page":"209","DOI":"10.3233\/sat190012","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisf. Boolean Model. Comput. 1(3\u20134), 209\u2013236 (2007). https:\/\/doi.org\/10.3233\/sat190012","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. In: Barrett, C.W., Yang, J. (eds.) FMCAD 2019, pp. 221\u2013230 (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894271","DOI":"10.23919\/FMCAD.2019.8894271"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-030-25543-5_24","volume-title":"Computer Aided Verification","author":"F Frohn","year":"2019","unstructured":"Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 426\u2013444. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_24"},{"key":"21_CR17","doi-asserted-by":"publisher","unstructured":"Frohn, F., Naaf, M., Brockschmidt, M., Giesl, J.: Inferring lower runtime bounds for integer programs. ACM Trans. Program. Lang. Syst. 42(3), 13:1\u201313:50 (2020). https:\/\/doi.org\/10.1145\/3410331","DOI":"10.1145\/3410331"},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 712\u2013722. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_41","DOI":"10.1007\/978-3-031-10769-6_41"},{"key":"21_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-031-38499-8_13","volume-title":"CADE 2023","author":"F Frohn","year":"2023","unstructured":"Frohn, F., Giesl, J.: Proving non-termination by acceleration driven clause learning. In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 220\u2013233. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_13"},{"key":"21_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-031-44245-2_13","volume-title":"SAS 2023","author":"F Frohn","year":"2023","unstructured":"Frohn, F., Giesl, J.: ADCL: acceleration driven clause learning for constrained horn clauses. In: Hermenegildo, M.V., Morales, J.F. (eds.) SAS 2023. LNCS, vol. 14284, pp. 259\u2013285. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_13"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Satisfiability modulo exponential integer arithmetic. CoRR abs\/2402.01501 (2024). https:\/\/doi.org\/10.48550\/arXiv.2402.01501","DOI":"10.48550\/arXiv.2402.01501"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Frohn, F., Giesl, J.: Evaluation of \u201cSatisfiability modulo exponential integer arithmetic\u201d (2024). https:\/\/aprove-developers.github.io\/swine-eval\/","DOI":"10.1007\/978-3-031-63498-7_21"},{"key":"21_CR23","unstructured":"Frohn, F., Giesl, J.: SwInE (2024). https:\/\/ffrohn.github.io\/swine\/"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$-complete decision procedures for satisfiability\u00a0over\u00a0the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_23"},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-030-17502-3_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Giesl","year":"2019","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 156\u2013166. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10"},{"key":"21_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00440-z","author":"M Hark","year":"2023","unstructured":"Hark, M., Frohn, F., Giesl, J.: Termination of triangular polynomial loops. Form. Methods Syst. Des. (2023). https:\/\/doi.org\/10.1007\/s10703-023-00440-z","journal-title":"Form. Methods Syst. Des."},{"key":"21_CR27","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. In: STRATA\u00a02003, pp. 56\u201368. Report NASA\/CP-2003-212448 (2003). https:\/\/apps.dtic.mil\/sti\/pdfs\/ADA418902.pdf"},{"key":"21_CR28","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Jagannathan, S., Sewell, P. (eds.) POPL 2014, pp. 529\u2013540 (2014). https:\/\/doi.org\/10.1145\/2535838.2535843","DOI":"10.1145\/2535838.2535843"},{"key":"21_CR29","doi-asserted-by":"publisher","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. Formal Methods Syst. Des. 47(1), 75\u201392 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0228-1","DOI":"10.1007\/s10703-015-0228-1"},{"key":"21_CR30","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-031-33170-1_29","volume-title":"NFM 2023","author":"E Lipparini","year":"2023","unstructured":"Lipparini, E., Ratschan, S.: Satisfiability of non-linear transcendental arithmetic as a certificate search problem. In: Rozier, K.Y., Chaudhuri, S. (eds.) NFM 2023. LNCS, vol. 13903, pp. 472\u2013488. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_29"},{"key":"21_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-030-80223-3_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: SMT-Switch: a solver-agnostic C++ API for SMT solving. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 377\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_26"},{"key":"21_CR32","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":"21_CR33","doi-asserted-by":"publisher","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"21_CR34","unstructured":"Termination Problems Data Base (TPDB). http:\/\/termination-portal.org\/wiki\/TPDB"},{"key":"21_CR35","doi-asserted-by":"publisher","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-63498-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:32Z","timestamp":1747592252000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}