{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T20:37:38Z","timestamp":1773952658371,"version":"3.50.1"},"publisher-location":"Cham","reference-count":68,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031747755","type":"print"},{"value":"9783031747762","type":"electronic"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-74776-2_14","type":"book-chapter","created":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:35:42Z","timestamp":1737351342000},"page":"352-385","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["An Order Theory Framework of\u00a0Recurrence Equations for\u00a0Static Cost Analysis \u2013 Dynamic Inference of\u00a0Non-Linear Inequality Invariants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1599-2431","authenticated-orcid":false,"given":"Louis","family":"Rustenholz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1092-2071","authenticated-orcid":false,"given":"Pedro","family":"L\u00f3pez-Garc\u00eda","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9782-8135","authenticated-orcid":false,"given":"Jos\u00e9 F.","family":"Morales","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7583-323X","authenticated-orcid":false,"given":"Manuel V.","family":"Hermenegildo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,21]]},"reference":[{"issue":"2","key":"14_CR1","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2), 161\u2013203 (2011)","journal-title":"J. Autom. Reason."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-030-45237-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Albert","year":"2020","unstructured":"Albert, E., Correas, J., Gordillo, P., Rom\u00e1n-D\u00edez, G., Rubio, A.: GASOL: gas analysis and optimization for ethereum smart contracts. In: TACAS 2020. LNCS, vol. 12079, pp. 118\u2013125. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_7"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Amrollahi, D., Bartocci, E., Kenison, G., Kov\u00e1cs, L., Moosbrugger, M., Stankovi\u010d, M.: (Un)Solvable loop analysis. arXiv 2306.01597 (2023)","DOI":"10.1007\/s10703-024-00455-0"},{"key":"14_CR4","unstructured":"Andersen, M.S., Dahl, J., Vandenberghe, L.: CVXOPT: a python package for convex optimization, version 1.3.2 (2023), available at https:\/\/cvxopt.org\/"},{"issue":"6","key":"14_CR5","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1016\/j.orl.2006.12.010","volume":"35","author":"DL Applegate","year":"2007","unstructured":"Applegate, D.L., Cook, W., Dash, S., Espinoza, D.G.: Exact solutions to linear programming problems. Oper. Res. Lett. 35(6), 693\u2013699 (2007)","journal-title":"Oper. Res. Lett."},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Formal Methods in Programming and Their Applications","author":"F Bourdoncle","year":"1993","unstructured":"Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bj\u00f8rner, D., Broy, M., Pottosin, I.V. (eds.) FMP &TA 1993. LNCS, vol. 735, pp. 128\u2013141. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0039704"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979, pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"key":"14_CR8","volume-title":"Principles of Abstract Interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"14_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088","volume-title":"Introduction to Lattices and Order","author":"BA Davey","year":"2002","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)","edition":"2"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Debray, S.K., Lin, N.W.: Cost analysis of logic programs. TOPLAS (1993)","DOI":"10.1145\/161468.161472"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Debray, S.K., Lin, N.W., Hermenegildo, M.V.: Task granularity analysis in logic programs. In: Proceedings of PLDI 1990, pp. 174\u2013188. ACM (1990)","DOI":"10.1145\/93542.93564"},{"key":"14_CR12","unstructured":"Debray, S.K., Lopez-Garcia, P., Hermenegildo, M.V., Lin, N.W.: Lower bound cost estimation for logic programs. In: ILPS 1997, pp. 291\u2013305. MIT Press (1997)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Dom\u00e9nech, J.J., Gallagher, J.P., Genaim, S.: Control-flow refinement by partial evaluation, and its application to termination and cost analysis. TPLP (2019)","DOI":"10.1017\/S1471068419000310"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Ernst, M., Cockrell, J., Griswold, W., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw, Eng (2001)","DOI":"10.1109\/32.908957"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-24725-8_4","volume-title":"Programming Languages and Systems","author":"J Feret","year":"2004","unstructured":"Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33\u201348. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_4"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-540-30579-8_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Feret","year":"2005","unstructured":"Feret, J.: The arithmetic-geometric progression abstract domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 42\u201358. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_3"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics. CUP (2009)","DOI":"10.1017\/CBO9780511801655"},{"key":"14_CR18","unstructured":"Flores-Montoya, A.: Cost Analysis of Programs Based on the Refinement of Cost Relations. Ph.D. thesis, T.U. Darmstadt (2017). Advisor: Reiner H\u00e4hnle"},{"key":"14_CR19","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-031-10769-6_41","volume-title":"IJCAR 2022","author":"F Frohn","year":"2022","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). 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"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Giesl, J., Lommen, N., Hark, M., Meyer, F.: Improving automatic complexity analysis of integer programs. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds.) The Logic of Software. A Tasting Menu of Formal Methods. LNCS, vol. 13360, pp. 193\u2013228. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08166-8_10","DOI":"10.1007\/978-3-031-08166-8_10"},{"key":"14_CR21","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":"14_CR22","doi-asserted-by":"crossref","unstructured":"Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Proceedings of HSCC 2017, pp. 1\u201310. ACM (2017)","DOI":"10.1145\/3049797.3049811"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-319-96142-2_31","volume-title":"Computer Aided Verification","author":"E Goubault","year":"2018","unstructured":"Goubault, E., Putot, S., Sahlmann, L.: Inner and outer approximating flowpipes for delay differential equations. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 523\u2013541. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_31"},{"key":"14_CR24","volume-title":"Concrete Mathematics","author":"RL Graham","year":"1989","unstructured":"Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics. Addison-Wesley, Hoboken (1989)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Hastie, T., Tibshirani, R., Wainwright, M.: Statistical Learning with Sparsity: The Lasso and Generalizations. Chapman & Hall\/CRC (2015)","DOI":"10.1201\/b18401"},{"issue":"1\u20132","key":"14_CR26","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.scico.2005.02.006","volume":"58","author":"M Hermenegildo","year":"2005","unstructured":"Hermenegildo, M., Puebla, G., Bueno, F., Lopez-Garcia, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the ciao system preprocessor). Sci. Comp. Progr. 58(1\u20132), 115\u2013140 (2005)","journal-title":"Sci. Comp. Progr."},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM TOPLAS 34(3), 14:1\u201314:62 (2012)","DOI":"10.1145\/2362389.2362393"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Humenberger, A., Jaroschek, M., Kov\u00e1cs, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences, pp. 221\u2013228. ISSAC 2017 (2017)","DOI":"10.1145\/3087604.3087623"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Ishimwe, D., Nguyen, K., Nguyen, T.: Dynaplex: analyzing program complexity using dynamically inferred recurrence relations. In: OOPSLA (2021)","DOI":"10.1145\/3485515"},{"issue":"6","key":"14_CR30","doi-asserted-by":"publisher","first-page":"1136","DOI":"10.1145\/195613.195632","volume":"41","author":"R Karp","year":"1994","unstructured":"Karp, R.: Probabilistic recurrence relations. J. ACM 41(6), 1136\u20131150 (1994)","journal-title":"J. ACM"},{"issue":"2","key":"14_CR31","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1145\/322248.322255","volume":"28","author":"M Karr","year":"1981","unstructured":"Karr, M.: Summation in finite terms. J. ACM 28(2), 305\u2013350 (1981)","journal-title":"J. ACM"},{"issue":"3","key":"14_CR32","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/s000170050020","volume":"52","author":"C Kimberling","year":"1997","unstructured":"Kimberling, C.: Best lower and upper approximates to irrational numbers. Elem. Math. 52(3), 122\u2013126 (1997)","journal-title":"Elem. Math."},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. POPL (2018)","DOI":"10.1145\/3158142"},{"key":"14_CR34","unstructured":"Knaster, B.: Un th\u00e9or\u00e8me sur les fonctions d\u2019ensembles. Ann. Soc. Polon. Math. 6, 133\u2013134 (1928), with A. Tarski"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L.: Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. Ph.D. thesis, RISC, Johannes Kepler University Linz (2007). Advisors: Tudor Jebelean and Andrei Voronkov","DOI":"10.1109\/ISoLA.2006.46"},{"key":"14_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4220-8","volume-title":"Introduction to Diophantine Approximations","author":"S Lang","year":"1995","unstructured":"Lang, S.: Introduction to Diophantine Approximations, 2nd edn. Springer, New York (1995)","edition":"2"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Le Metayer, D.: ACE: an automatic complexity evaluator. TOPLAS (1988)","DOI":"10.1145\/42190.42347"},{"key":"14_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-6947-5","volume-title":"Difference Algebra Algebra and Applications","author":"A Levin","year":"2008","unstructured":"Levin, A.: Difference Algebra Algebra and Applications. Springer, New York (2008)"},{"key":"14_CR39","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-43369-6_1","volume-title":"FroCos 2023","author":"N Lommen","year":"2023","unstructured":"Lommen, N., Giesl, J.: Targeting completeness: using closed forms for size bounds of integer programs. In: Sattler, U., Suda, M. (eds.) FroCos 2023. LNCS, vol. 14279, pp. 3\u201322. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43369-6_1"},{"issue":"2","key":"14_CR40","first-page":"167","volume":"18","author":"P Lopez-Garcia","year":"2018","unstructured":"Lopez-Garcia, P., Darmawan, L., Klemen, M., Liqat, U., Bueno, F., Hermenegildo, M.V.: Interval-based resource usage verification by translation into horn clauses and an application to energy consumption. TPLP 18(2), 167\u2013223 (2018)","journal-title":"TPLP"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Lopez-Garcia, P., Klemen, M., Liqat, U., Hermenegildo, M.V.: A general framework for static profiling of parametric resource usage. In: ICLP (2016)","DOI":"10.1017\/S1471068416000442"},{"key":"14_CR42","unstructured":"Lv, M., Guan, N., Reineke, J., Wilhelm, R., Yi, W.: A survey on static cache analysis for real-time systems. LITES 3(1), 05:1\u201305:48 (2016)"},{"key":"14_CR43","unstructured":"Wolfram Mathematica (v13.2): The World\u2019s Definitive System for Modern Technical Computing. https:\/\/www.wolfram.com\/mathematica. Accessed 25 May 2023"},{"key":"14_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-642-02658-4_42","volume-title":"Computer Aided Verification","author":"D Monniaux","year":"2009","unstructured":"Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 570\u2013583. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_42"},{"key":"14_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-74610-2_24","volume-title":"Logic Programming","author":"J Navas","year":"2007","unstructured":"Navas, J., Mera, E., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.V.: User-definable resource bounds analysis for logic programs. In: Dahl, V., Niemel\u00e4, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 348\u2013363. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74610-2_24"},{"issue":"1","key":"14_CR46","first-page":"21","volume":"105","author":"N Nedialkov","year":"1999","unstructured":"Nedialkov, N., Jackson, K., Corliss, G.: Validated solutions of initial value problems for ordinary differential equations. Appl. Math. Comput. 105(1), 21\u201368 (1999)","journal-title":"Appl. Math. Comput."},{"key":"14_CR47","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE (2012)","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"14_CR48","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to generate disjunctive invariants. In: ICSE (2014)","DOI":"10.1145\/2568225.2568275"},{"issue":"10","key":"14_CR49","doi-asserted-by":"publisher","first-page":"3877","DOI":"10.1109\/TSE.2021.3106964","volume":"48","author":"T Nguyen","year":"2022","unstructured":"Nguyen, T., Nguyen, K., Dwyer, M.B.: Using symbolic states to infer numerical invariants. IEEE Trans. Software Eng. 48(10), 3877\u20133899 (2022)","journal-title":"IEEE Trans. Software Eng."},{"key":"14_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-030-65474-0_2","volume-title":"Static Analysis","author":"V P\u00e9rez","year":"2020","unstructured":"P\u00e9rez, V., Klemen, M., L\u00f3pez-Garc\u00eda, P., Morales, J.F., Hermenegildo, M.: Cost analysis of smart contracts via parametric resource analysis. In: Pichardie, D., Sighireanu, M. (eds.) SAS 2020. LNCS, vol. 12389, pp. 7\u201331. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-65474-0_2"},{"issue":"2","key":"14_CR51","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0747-7171(92)90038-6","volume":"14","author":"M Petkov\u0161ek","year":"1992","unstructured":"Petkov\u0161ek, M.: Hypergeometric solutions of linear recurrences with polynomial coefficients. J. Symb. Comput. 14(2), 243\u2013264 (1992)","journal-title":"J. Symb. Comput."},{"key":"14_CR52","doi-asserted-by":"publisher","unstructured":"Petkov\u0161ek, M., Zakraj\u0161ek, H.: Solving linear recurrence equations with polynomial coefficients. In: Schneider, C., Bl\u00fcmlein, J. (eds) Computer Algebra in Quantum Field Theory: Integration, Summation and Special Functions, pp. 259\u2013284. Springer, Vienna (2013). https:\/\/doi.org\/10.1007\/978-3-7091-1616-6_11","DOI":"10.1007\/978-3-7091-1616-6_11"},{"key":"14_CR53","doi-asserted-by":"crossref","unstructured":"Pham, L., Saad, F.A., Hoffmann, J.: Robust resource bounds with static analysis and Bayesian inference. In: PLDI (2024)","DOI":"10.1145\/3656380"},{"issue":"1","key":"14_CR54","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1016\/j.scico.2006.03.003","volume":"64","author":"E Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54\u201375 (2007). Special issue on SAS 2004","journal-title":"Sci. Comput. Program."},{"key":"14_CR55","doi-asserted-by":"crossref","unstructured":"Rosendahl, M.: Automatic complexity analysis. In: FPCA (1989)","DOI":"10.1145\/99370.99381"},{"key":"14_CR56","unstructured":"Rustenholz, L.: Automated approximate recurrence solving applied to static analysis of energy consumption. Technical report, CLIP Lab, IMDEA Software Institute (2022). https:\/\/cliplab.org\/papers\/rustenholz-aars-msc.pdf"},{"key":"14_CR57","doi-asserted-by":"crossref","unstructured":"Rustenholz, L., Klemen, M., Carreira-Perpi\u00f1\u00e1n, M.\u00c1., L\u00f3pez-Garc\u00eda, P.: A machine learning-based approach for solving recurrence relations and its use in cost analysis of logic programs. TPLP (2024). https:\/\/www.doi.org\/10.1017\/S1471068424000413","DOI":"10.1017\/S1471068424000413"},{"key":"14_CR58","unstructured":"Rustenholz, L., Lopez-Garcia, P., Morales, J.F., Hermenegildo, M.V.: An order theory framework of recurrence equations for static cost analysis - dynamic inference of non-linear inequality invariants (2024). https:\/\/arxiv.org\/abs\/2406.18260, (Extended\/preprint version of this paper)"},{"key":"14_CR59","doi-asserted-by":"publisher","unstructured":"Rustenholz, L., Lopez-Garcia, P., Morales, J.F., Hermenegildo, M.: Artifact for \u201can order theory framework of recurrence equations for static cost analysis \u2013 dynamic inference of non-linear inequality invariants\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.13133801","DOI":"10.5281\/zenodo.13133801"},{"key":"14_CR60","doi-asserted-by":"crossref","unstructured":"Serrano, A., Lopez-Garcia, P., Hermenegildo, M.V.: Resource usage analysis of logic programs via abstract interpretation using sized types. ICLP (2014)","DOI":"10.1017\/S147106841400057X"},{"issue":"1","key":"14_CR61","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9402-4","volume":"59","author":"M Sinn","year":"2017","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason. 59(1), 3\u201345 (2017)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"14_CR62","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1137\/0211062","volume":"11","author":"MB Smyth","year":"1982","unstructured":"Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput. 11(4), 761\u2013783 (1982)","journal-title":"SIAM J. Comput."},{"key":"14_CR63","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-031-37709-9_2","volume-title":"CAV 2023","author":"Y Sun","year":"2023","unstructured":"Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Automated tail bound analysis for probabilistic recurrence relations. In: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13966, pp. 16\u201339. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_2"},{"issue":"2","key":"14_CR64","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"issue":"OOPSLA1","key":"14_CR65","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/3586028","volume":"7","author":"C Wang","year":"2023","unstructured":"Wang, C., Lin, F.: Solving conditional linear recurrences for program verification: the periodic case. Proc. ACM Program. Lang. 7(OOPSLA1), 28\u201355 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"14_CR66","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 (2021)","DOI":"10.1145\/3410310"},{"issue":"9","key":"14_CR67","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528\u2013539 (1975). https:\/\/doi.org\/10.1145\/361002.361016","journal-title":"Commun. ACM"},{"key":"14_CR68","doi-asserted-by":"crossref","unstructured":"Westrick, S., Fluet, M., Rainey, M., Acar, U.A.: Automatic parallelism management. In: POPL (2024)","DOI":"10.1145\/3632880"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74776-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:36:00Z","timestamp":1737351360000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74776-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031747755","9783031747762"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74776-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"20 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2024.splashcon.org\/home\/sas-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}