{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T09:10:11Z","timestamp":1746522611241,"version":"3.40.4"},"publisher-location":"Cham","reference-count":95,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911200"},{"type":"electronic","value":"9783031911217"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Recurrence relations are used in a wide variety of static program analysis tasks such as loop summarization, invariant generation, and, most classically, modeling the (asymptotic) worst-case runtime behavior of recursive divide-and-conquer algorithms. In this work, we focus on the latter use-case. Classical methods for this problem, such as the well-known Master Theorem (MT) or the Akra-Bazzi method (AB) can only handle <jats:italic>single<\/jats:italic> recurrences of a certain limited form. Specifically, MT requires that each instance be divided into a <jats:italic>fixed<\/jats:italic> number of smaller sub-instances of the <jats:italic>same size<\/jats:italic>. AB generalizes MT by allowing sub-instances of different sizes, but still requires that the number of such sub-instances be fixed and independent of the size of the original instance. Moreover, these methods can handle neither <jats:italic>multi-variate<\/jats:italic> recurrences nor <jats:italic>systems<\/jats:italic> of recurrences that model non-simple recursive behavior among two or more procedures.<\/jats:p>\n          <jats:p>In this work, we lift these restrictions and consider a wide family of recurrences called Generalized Polynomial Recurrence Systems (GPRS). Our setting is highly expressive and allows systems of multi-variate recurrences in which an instance can be divided into polynomially-many sub-instances. Moreover, the division is not limited to a single rule and can have several cases based on conditions on the values of the variables. We show how to obtain polynomial upper-bounds for a GPRS using template-based methods and classical theorems from polyhedral and algebraic geometry. Our approach reduces the synthesis of polynomial upper-bounds to linear or semi-definite programming instances, enabling efficient solutions. Crucially, our method is sound and semi-complete, i.e.\u00a0complete for polynomials of any fixed degree and obtains concrete, as opposed to asymptotic, upper-bounds.<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_1","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:07:49Z","timestamp":1746184069000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Synthesis of Tight Polynomial Upper-Bounds for Systems of Conditional Polynomial Recurrences"],"prefix":"10.1007","author":[{"given":"Amir K.","family":"Goharshady","sequence":"first","affiliation":[]},{"given":"S.","family":"Hitarth","sequence":"additional","affiliation":[]},{"given":"Sergei","family":"Novozhilov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Akra, M.A., Bazzi, L.: On the solution of linear recurrence equations. Comput. Optim. Appl. 10(2), 195\u2013210 (1998)","DOI":"10.1023\/A:1018373005182"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Akshay, S., Chakraborty, S., Goharshady, A.K., Govind, R., Motwani, H.J., Varanasi, S.T.: Automated synthesis of decision lists for polynomial specifications over integers. In: LPAR. pp. 484\u2013502 (2024)","DOI":"10.29007\/njph"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Akshay, S., Chakraborty, S., Goharshady, A.K., Govind, R., Motwani, H.J., Varanasi, S.T.: Practical approximate quantifier elimination for non-linear real arithmetic. In: FM. pp. 111\u2013130 (2024)","DOI":"10.1007\/978-3-031-71162-6_6"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: SAS. pp. 221\u2013237 (2008)","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"1_CR5","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: PUBS: a practical upper bounds solver. https:\/\/costa.fdi.ucm.es\/~costa\/pubs\/examples.php (2008)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: PLDI. pp. 772\u2013787 (2021)","DOI":"10.1145\/3453483.3454076"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Log. Methods Comput. Sci. 7(2) (2011)","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: TACAS. pp. 415\u2013442 (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: Cvc4. In: CAV. pp. 171\u2013177 (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: ATVA. pp. 255\u2013276 (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Existential theory of the reals. Algorithms in Real Algebraic Geometry pp. 505\u2013532 (2006)","DOI":"10.1007\/3-540-33099-2_14"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Bentley, J.L., Haken, D., Saxe, J.B.: A general method for solving divide-and-conquer recurrences. SIGACT News 12(3), 36\u201344 (1980)","DOI":"10.1145\/1008861.1008865"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: TACAS. pp. 495\u2013522 (2023)","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Blekherman, G., Parrilo, P.A., Thomas, R.R.: Semidefinite optimization and convex algebraic geometry (2012)","DOI":"10.1137\/1.9781611972290"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Breck, J., Cyphert, J., Kincaid, Z., Reps, T.W.: Templates and recurrences: better together. In: PLDI. pp. 688\u2013702 (2020)","DOI":"10.1145\/3385412.3386035"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Cai, Z., Farokhnia, S., Goharshady, A.K., Hitarth, S.: Asparagus: Automated synthesis of parametric gas upper-bounds for smart contracts. Proc. ACM Program. Lang. 7(OOPSLA2), 882\u2013911 (2023)","DOI":"10.1145\/3622829"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Campbell, B.: Amortised memory analysis using the depth of data structures. In: ESOP. vol.\u00a05502, pp. 190\u2013204 (2009)","DOI":"10.1007\/978-3-642-00590-9_14"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. In: STOC. pp. 460\u2013467 (1988)","DOI":"10.1145\/62212.62257"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: PLDI. pp. 270\u2013281 (2014)","DOI":"10.1145\/2594291.2594301"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Reps, T.W., Shao, Z.: Automated resource analysis with Coq proof objects. In: CAV. pp. 64\u201385 (2017)","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: PLDI. pp. 467\u2013478 (2015)","DOI":"10.1145\/2737924.2737955"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. 62(3), 331\u2013365 (2019)","DOI":"10.1007\/s10817-017-9431-7"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: CAV. pp. 3\u201322 (2016)","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. In: CAV. vol. 10427, pp. 41\u201363 (2017)","DOI":"10.1007\/978-3-319-63390-9_3"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Non-polynomial worst-case analysis of recursive programs. ACM Trans. Program. Lang. Syst. 41(4), 20:1\u201320:52 (2019)","DOI":"10.1145\/3339984"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: PLDI. pp. 672\u2013687 (2020)","DOI":"10.1145\/3385412.3385969"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Okati, N.: Computational approaches for stochastic shortest path on succinct MDPs. In: IJCAI. pp. 4700\u20134707 (2018)","DOI":"10.24963\/ijcai.2018\/653"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: POPL. pp. 327\u2013342 (2016)","DOI":"10.1145\/2837614.2837639"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Goharshady, E.K., Karrabi, M., Zikelic, D.: Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In: FM. pp. 600\u2013619 (2024)","DOI":"10.1007\/978-3-031-71162-6_31"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Goyal, P., Ibsen-Jensen, R., Pavlogiannis, A.: Faster algorithms for dynamic algebraic queries in basic RSMs with constant treewidth. ACM Trans. Program. Lang. Syst. 41(4), 23:1\u201323:46 (2019)","DOI":"10.1145\/3363525"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Ibsen-Jensen, R., Pavlogiannis, A.: Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: POPL. pp. 733\u2013747 (2016)","DOI":"10.1145\/2837614.2837624"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: CAV. pp. 55\u201378 (2022)","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Quantitative bounds on resource usage of probabilistic programs. Proc. ACM Program. Lang. 8(OOPSLA1), 362\u2013391 (2024)","DOI":"10.1145\/3649824"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Ibsen-Jensen, R., Goharshady, A.K., Pavlogiannis, A.: Algorithms for algebraic path properties in concurrent systems of constant treewidth components. ACM Trans. Program. Lang. Syst. 40(3), 9:1\u20139:43 (2018)","DOI":"10.1145\/3210257"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Dubhashi, D.P.: Probabilistic recurrence relations revisited. Theor. Comput. Sci. 181(1), 45\u201356 (1997)","DOI":"10.1016\/S0304-3975(96)00261-7"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: CAV. pp. 420\u2013432 (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Conrado, G.K., Goharshady, A.K., Kochekov, K., Tsai, Y.C., Zaher, A.K.: Exploiting the sparseness of control-flow and call graphs for efficient and on-demand algebraic program analysis. Proc. ACM Program. Lang. 7(OOPSLA2), 1993\u20132022 (2023)","DOI":"10.1145\/3622868"},{"key":"1_CR38","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms (1990)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Cygan, M., Fomin, F.V., Kowalik, \u0141., Lokshtanov, D., Marx, D., Pilipczuk, M., Pilipczuk, M., Saurabh, S.: Parameterized algorithms (2015)","DOI":"10.1007\/978-3-319-21275-3"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Cyphert, J., Kincaid, Z.: Solvable polynomial ideals: The ideal reflection for program analysis. Proc. ACM Program. Lang. 8(POPL), 724\u2013752 (2024)","DOI":"10.1145\/3632867"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Das, A., Balzer, S., Hoffmann, J., Pfenning, F., Santurkar, I.: Resource-aware session types for digital contracts. In: CSF. pp. 1\u201316 (2021)","DOI":"10.1109\/CSF51468.2021.00004"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Das, A., Hoffmann, J., Pfenning, F.: Work analysis with resource-aware session types. In: LICS. pp. 305\u2013314 (2018)","DOI":"10.1145\/3209108.3209146"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Das, A., Qadeer, S.: Exact and linear-time gas-cost analysis. In: SAS. vol. 12389, pp. 333\u2013356 (2020)","DOI":"10.1007\/978-3-030-65474-0_15"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Downey, R.G., Fellows, M.R.: Parameterized complexity (2012)","DOI":"10.1007\/978-1-4471-5559-1"},{"key":"1_CR45","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. J. ACM 57(6), 33:1\u201333:47 (2010)","DOI":"10.1145\/1857914.1857917"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Farkas, J.: Theorie der einfachen ungleichungen (in German). Journal f\u00fcr die reine und angewandte Mathematik 1902(124), 1\u201327 (1902)","DOI":"10.1515\/crll.1902.124.1"},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD. pp. 57\u201364 (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"1_CR48","doi-asserted-by":"crossref","unstructured":"Fomin, F.V., Grandoni, F., Kratsch, D.: A measure & conquer approach for the analysis of exact algorithms. J. ACM 56(5), 25:1\u201325:32 (2009)","DOI":"10.1145\/1552285.1552286"},{"key":"1_CR49","unstructured":"Goharshady, A.: Parameterized and Algebro-geometric Advances in Static Program Analysis. Ph.D. thesis, Institute of Science and Technology Austria (Nov 2020), https:\/\/hal.science\/tel-03153209"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Goharshady, A.K., Hitarth, S., Mohammadi, F., Motwani, H.J.: Algebro-geometric algorithms for template-based synthesis of polynomial programs. In: OOPSLA. pp. 727\u2013756 (2023)","DOI":"10.1145\/3586052"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics 132(1), 35\u201362 (1988)","DOI":"10.2140\/pjm.1988.132.35"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Heintz, J., Roy, M.F., Solern\u00f3, P.: Sur la complexit\u00e9 du principe de Tarski-Seidenberg (in French). Bulletin de la Soci\u00e9t\u00e9 math\u00e9matique de France 118(1), 101\u2013126 (1990)","DOI":"10.24033\/bsmf.2138"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012)","DOI":"10.1145\/2362389.2362393"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: CAV. pp. 781\u2013786 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_64","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. https:\/\/www.raml.co\/ (2012)","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In: APLAS. pp. 172\u2013187 (2010)","DOI":"10.1007\/978-3-642-17164-2_13"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: ESOP. pp. 287\u2013306 (2010)","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Jost, S.: Two decades of automatic amortized resource analysis. Math. Struct. Comput. Sci. 32(6), 729\u2013759 (2022)","DOI":"10.1017\/S0960129521000487"},{"key":"1_CR59","unstructured":"Hofmann, M.: A type system for bounded space and functional in-place update. Nord. J. Comput. 7(4), 258\u2013289 (2000)"},{"key":"1_CR60","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Static prediction of heap space usage for first-order functional programs. In: POPL. pp. 185\u2013197 (2003)","DOI":"10.1145\/640128.604148"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: ESOP. pp. 22\u201337 (2006)","DOI":"10.1007\/11693024_3"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Rodriguez, D.: Efficient type-checking for amortised heap-space analysis. In: CSL. pp. 317\u2013331 (2009)","DOI":"10.1007\/978-3-642-04027-6_24"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang. 3(OOPSLA), 129:1\u2013129:29 (2019)","DOI":"10.1145\/3360555"},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences. In: ISSAC. pp. 221\u2013228 (2017)","DOI":"10.1145\/3087604.3087623"},{"key":"1_CR65","doi-asserted-by":"crossref","unstructured":"Ishimwe, D., Nguyen, K., Nguyen, T.: Dynaplex: analyzing program complexity using dynamically inferred recurrence relations. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201323 (2021)","DOI":"10.1145\/3485515"},{"key":"1_CR66","doi-asserted-by":"crossref","unstructured":"Jost, S., Vasconcelos, P.B., Florido, M., Hammond, K.: Type-based cost analysis for lazy functional languages. J. Autom. Reason. 59(1), 87\u2013120 (2017)","DOI":"10.1007\/s10817-016-9398-9"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"Kahn, D.M., Hoffmann, J.: Exponential automatic amortized resource analysis. In: FoSSaCS. pp. 359\u2013380 (2020)","DOI":"10.1007\/978-3-030-45231-5_19"},{"key":"1_CR68","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Probabilistic recurrence relations. In: STOC. pp. 190\u2013197. ACM (1991)","DOI":"10.1145\/103418.103443"},{"key":"1_CR69","doi-asserted-by":"crossref","unstructured":"Karp, R.M.: Probabilistic recurrence relations. J. ACM 41(6), 1136\u20131150 (1994)","DOI":"10.1145\/195613.195632"},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: PLDI. pp. 248\u2013262 (2017)","DOI":"10.1145\/3062341.3062373"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Reps, T.W., Cyphert, J.: Algebraic program analysis. In: CAV. pp. 46\u201383 (2021)","DOI":"10.1007\/978-3-030-81685-8_3"},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L.: Reasoning algebraically about p-solvable loops. In: TACAS. pp. 249\u2013264 (2008)","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: CAV. pp. 1\u201335 (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"1_CR74","unstructured":"Kov\u00e1cs, L., Jebelean, T.: Automated generation of loop invariants by recurrence solving in theorema (01 2004)"},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Lin, F.: A formalization of programs in first-order logic with a discrete linear order. Artif. Intell. 235, 1\u201325 (2016)","DOI":"10.1016\/j.artint.2016.01.014"},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Liu, H., Fu, H., Yu, Z., Song, J., Li, G.: Scalable linear invariant generation with Farkas\u2019 lemma. In: OOPSLA. pp. 204\u2013232 (2022)","DOI":"10.1145\/3563295"},{"key":"1_CR77","unstructured":"Macintyre, A., Wilkie, A.J., Odifreddi, P.: On the decidability of the real exponential field. Kreisel\u2019s Mathematics 115, \u00a0451 (1996)"},{"key":"1_CR78","unstructured":"Moosbrugger, M., Amrollahi, D., M\u00fcllner, J., Kenison, G., Kofnov, A.: Polar github repository. https:\/\/github.com\/probing-lab\/polar (2023)"},{"key":"1_CR79","unstructured":"MOSEK ApS: Mosek optimization suite (2023), https:\/\/docs.mosek.com\/10.0\/intro.pdf"},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: TACAS. pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1_CR81","doi-asserted-by":"publisher","unstructured":"Novozhilov, S., Hitarth, S., Kafshdar\u00a0Goharshady, A.: polyrecur: A C++ tool based on SDP solvers for solving generalized polynomial recurrence systems (GPRS) (2025). https:\/\/doi.org\/10.5281\/zenodo.14836308","DOI":"10.5281\/zenodo.14836308"},{"key":"1_CR82","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI. vol.\u00a02937, pp. 239\u2013251 (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"1_CR83","doi-asserted-by":"crossref","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana University Mathematics Journal 42(3), 969\u2013984 (1993)","DOI":"10.1512\/iumj.1993.42.42045"},{"key":"1_CR84","doi-asserted-by":"crossref","unstructured":"Reps, T.W., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. In: POPL. pp. 663\u2013677 (2016)","DOI":"10.1145\/2837614.2837659"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: POPL. pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"key":"1_CR86","unstructured":"Schoutens, H.: Muchnik\u2019s proof of Tarski-Seidenberg. Ohio State University (2001)"},{"key":"1_CR87","unstructured":"Semenov, A.: Decision procedures for logical theories (in Russian). Cybernetics and computer technology 2, 134\u2013146 (1986)"},{"key":"1_CR88","doi-asserted-by":"crossref","unstructured":"Strassen, V.: Gaussian elimination is not optimal. Numerische Mathematik 13(4), 354\u2013356 (1969)","DOI":"10.1007\/BF02165411"},{"key":"1_CR89","doi-asserted-by":"crossref","unstructured":"Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Automated tail bound analysis for probabilistic recurrence relations. In: CAV. pp. 16\u201339 (2023)","DOI":"10.1007\/978-3-031-37709-9_2"},{"key":"1_CR90","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Harper, R.: Verified tail bounds for randomized programs. In: ITP. pp. 560\u2013578 (2018)","DOI":"10.1007\/978-3-319-94821-8_33"},{"key":"1_CR91","doi-asserted-by":"crossref","unstructured":"Wang, C., Lin, F.: Solving conditional linear recurrences for program verification: The periodic case. In: OOPSLA. pp. 28\u201355 (2023)","DOI":"10.1145\/3586028"},{"key":"1_CR92","doi-asserted-by":"crossref","unstructured":"Wang, D., Kahn, D.M., Hoffmann, J.: Raising expectations: automating expected cost analysis with types. Proc. ACM Program. Lang. 4(ICFP), 110:1\u2013110:31 (2020)","DOI":"10.1145\/3408992"},{"key":"1_CR93","doi-asserted-by":"crossref","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: PLDI. pp. 1171\u20131186 (2021)","DOI":"10.1145\/3453483.3454102"},{"key":"1_CR94","doi-asserted-by":"crossref","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: PLDI. pp. 204\u2013220 (2019)","DOI":"10.1145\/3314221.3314581"},{"key":"1_CR95","unstructured":"Watkins, D.S.: Fundamentals of matrix computations (2004)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:40:26Z","timestamp":1746520826000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":95,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}