{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T14:54:33Z","timestamp":1781708073649,"version":"3.54.5"},"reference-count":100,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T00:00:00Z","timestamp":1773878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T00:00:00Z","timestamp":1773878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003759","name":"Universidad Polit\u00e9cnica de Madrid","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003759","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present theoretical and practical results on the order theory of lattices of functions, focusing on Galois connections that abstract (sets of) functions \u2013 a topic known as\n                    <jats:italic>higher-order abstract interpretation<\/jats:italic>\n                    . We are motivated by the challenge of inferring closed-form bounds on functions which are defined recursively, i.e. as the fixed point of an operator or, equivalently, as the solution to a functional equation. This has multiple applications in program analysis (e.g. cost analysis, loop acceleration, declarative language analysis) and in hybrid systems governed by differential equations. Our main contribution is a new family of constraint-based abstract domains for abstracting numerical functions,\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$\\mathfrak {B}$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>B<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    <jats:italic>-bound domains<\/jats:italic>\n                    , which abstract a function\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$f$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>f<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    by a conjunction of bounds from a preselected set of boundary functions. They allow inferring\n                    <jats:italic>highly non-linear numerical invariants<\/jats:italic>\n                    , which classical numerical abstract domains struggle with. We uncover a\n                    <jats:italic>convexity property<\/jats:italic>\n                    in the constraint space that simplifies, and, in some cases, fully\n                    <jats:italic>automates<\/jats:italic>\n                    , transfer function design. We also introduce\n                    <jats:italic>domain abstraction<\/jats:italic>\n                    , a functor that lifts arbitrary mappings in value space to Galois connections in function space. This supports abstraction from symbolic to numerical functions (i.e.\n                    <jats:italic>size abstraction<\/jats:italic>\n                    ), and enables dimensionality reduction of equations. We base our constructions of transfer functions on a simple\n                    <jats:italic>operator language<\/jats:italic>\n                    , starting with\n                    <jats:italic>sequences<\/jats:italic>\n                    , and extending to more general\n                    <jats:italic>functions<\/jats:italic>\n                    , including multivariate, piecewise, and non-discrete domains.\n                  <\/jats:p>","DOI":"10.1007\/s10009-026-00843-3","type":"journal-article","created":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T09:15:52Z","timestamp":1773911752000},"page":"277-301","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Abstractions of sequences, functions and operators"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1599-2431","authenticated-orcid":false,"given":"Louis","family":"Rustenholz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1092-2071","authenticated-orcid":false,"given":"Pedro","family":"Lopez-Garcia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7583-323X","authenticated-orcid":false,"given":"Manuel V.","family":"Hermenegildo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,3,19]]},"reference":[{"key":"843_CR1","unstructured":"Wolfram Mathematica (v13.2): the World\u2019s Definitive System for Modern Technical Computing https:\/\/www.wolfram.com\/mathematica. Accessed: May 25, 2023"},{"key":"843_CR2","doi-asserted-by":"crossref","unstructured":"Adj\u00e9, A., Gaubert, S., Goubault, E.: Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. LMCS 8(1) (2011)","DOI":"10.2168\/LMCS-8(1:1)2012"},{"key":"843_CR3","volume-title":"Compilers - Principles, Techniques and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers - Principles, Techniques and Tools. Addison-Wesley, Reading (1986)"},{"key":"843_CR4","doi-asserted-by":"crossref","unstructured":"Aichinger, E., Aichinger, F.: Dickson\u2019s Lemma, Higman\u2019s Theorem and Beyond: a survey of some basic results in order theory. Expo. Math. 38(4) (2020)","DOI":"10.1016\/j.exmath.2019.05.003"},{"issue":"2","key":"843_CR5","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":"843_CR6","volume-title":"SAS","author":"X. Allamigeon","year":"2008","unstructured":"Allamigeon, X., Gaubert, S., Goubault, E.: Inferring min and max invariants using max-plus polyhedra. In: SAS (2008)"},{"key":"843_CR7","first-page":"124","volume-title":"The Language PCF","author":"R.M. Amadio","year":"1998","unstructured":"Amadio, R.M., Curien, P.L.: Domains and Lambda-Calculi. In: The Language PCF, pp.\u00a0124\u2013143. Cambridge University Press, Cambridge (1998)"},{"issue":"1","key":"843_CR8","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1), 28\u201356 (2005). Special Issue on SAS 2003","journal-title":"Sci. Comput. Program."},{"key":"843_CR9","unstructured":"Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: PURRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis. Tech. Rep. (2005). arXiv:cs\/0512056"},{"key":"843_CR10","volume-title":"SAS","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Rodr\u00edguez-Carbonell, E., Zaffanella, E.: Generation of basic semi-algebraic invariants using convex polyhedra. In: SAS (2005)"},{"issue":"4\u20135","key":"843_CR11","first-page":"449","volume":"8","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT 8(4\u20135), 449\u2013466 (2007)","journal-title":"STTT"},{"key":"843_CR12","doi-asserted-by":"crossref","unstructured":"Bautista, S., Jensen, T., Montagu, B.: An input\u2013output relational domain for algebraic data types and functional arrays. FMSD (2024)","DOI":"10.1007\/s10703-024-00456-z"},{"key":"843_CR13","doi-asserted-by":"crossref","unstructured":"Brauer, J., King, A.: Transfer function synthesis without quantifier elimination LMCS (2012)","DOI":"10.2168\/LMCS-8(3:17)2012"},{"key":"843_CR14","volume-title":"Functional Programming","author":"G.L. Burn","year":"1991","unstructured":"Burn, G.L.: The abstract interpretation of higher-order functional languages: from properties to abstract domains. In: Heldal, R., Holst, C.K., Wadler, P. (eds.) Functional Programming (1991)"},{"key":"843_CR15","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0167-6423(86)90010-9","volume":"7","author":"G.L. Burn","year":"1986","unstructured":"Burn, G.L., Hankin, C., Abramsky, S.: Strictness analysis for higher-order functions. Sci. Comput. Program. 7, 249\u2013278 (1986)","journal-title":"Sci. Comput. Program."},{"key":"843_CR16","doi-asserted-by":"crossref","unstructured":"Celaya, M., Ruskey, F.: An undecidable nested recurrence relation (2012). https:\/\/arxiv.org\/abs\/1203.0586","DOI":"10.1007\/978-3-642-30870-3_12"},{"key":"843_CR17","volume-title":"SAS","author":"J. Chen","year":"2015","unstructured":"Chen, J., Cousot, P.: A binary decision tree abstract domain functor. In: SAS (2015)"},{"key":"843_CR18","volume-title":"ATFL","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: ATFL (1975)"},{"key":"843_CR19","volume-title":"POPL","author":"P. Cousot","year":"1997","unstructured":"Cousot, P.: Types as abstract interpretations. In: POPL (1997)"},{"key":"843_CR20","volume-title":"Principles of Abstract Interpretation","author":"P. Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"843_CR21","volume-title":"ISOP","author":"P. Cousot","year":"1976","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: ISOP (1976)"},{"key":"843_CR22","volume-title":"ICCL","author":"P. Cousot","year":"1994","unstructured":"Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In: ICCL (1994)"},{"key":"843_CR23","first-page":"3","volume-title":"POPL","author":"P. Cousot","year":"2014","unstructured":"Cousot, P., Cousot, R.: A Galois connection calculus for abstract interpretation. In: POPL, pp.\u00a03\u20134. ACM, New York (2014)"},{"key":"843_CR24","volume-title":"POPL","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)"},{"key":"843_CR25","volume-title":"Cost Analysis of Logic Programs. TOPLAS","author":"S.K. Debray","year":"1993","unstructured":"Debray, S.K., Lin, N.W.: Cost Analysis of Logic Programs. TOPLAS (1993)"},{"key":"843_CR26","volume-title":"PLDI","author":"S.K. Debray","year":"1990","unstructured":"Debray, S.K., Lin, N.W., Hermenegildo, M.: Task granularity analysis in logic programs. In: PLDI (1990)"},{"key":"843_CR27","first-page":"291","volume-title":"ILPS\u201997","author":"S.K. Debray","year":"1997","unstructured":"Debray, S.K., Lopez-Garcia, P., Hermenegildo, M., Lin, N.W.: Lower bound cost estimation for logic programs. In: ILPS\u201997, pp.\u00a0291\u2013305. MIT Press, Cambridge (1997)"},{"issue":"1","key":"843_CR28","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1111\/j.1749-6632.1993.tb52513.x","volume":"704","author":"M. Ern\u00e9","year":"1993","unstructured":"Ern\u00e9, M., Koslowski, J., Melton, A., Strecker, G.E.: A primer on Galois connections. Ann. N.Y. Acad. Sci. 704(1), 103\u2013125 (1993)","journal-title":"Ann. N.Y. Acad. Sci."},{"key":"843_CR29","doi-asserted-by":"crossref","unstructured":"Feret, J.: Static Analysis of Digital Filters ESOP (2004)","DOI":"10.1007\/978-3-540-24725-8_4"},{"key":"843_CR30","doi-asserted-by":"crossref","unstructured":"Feret, J.: The Arithmetic-Geometric Progression Abstract Domain. VMCAI (2005)","DOI":"10.1007\/978-3-540-30579-8_3"},{"key":"843_CR31","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801655","volume-title":"Analytic Combinatorics","author":"P. Flajolet","year":"2009","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics. Cambridge University Press, Cambridge (2009)"},{"key":"843_CR32","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":"843_CR33","doi-asserted-by":"publisher","DOI":"10.1017\/9781108668804","volume-title":"An Invitation to Applied Category Theory: Seven Sketches in Compositionality","author":"B. Fong","year":"2019","unstructured":"Fong, B., Spivak, D.I.: An Invitation to Applied Category Theory: Seven Sketches in Compositionality. Cambridge University Press, Cambridge (2019)"},{"key":"843_CR34","unstructured":"Gomber, S., Banerjee, D., Singh, G.: Universal synthesis of differentiably tunable numerical abstract transformers (2025). https:\/\/arxiv.org\/abs\/2507.11827"},{"key":"843_CR35","first-page":"240","volume":"1899","author":"P. Gordan","year":"1899","unstructured":"Gordan, P.: Neuer Beweis des Hilbertschen Satzes \u00fcber homogene Funktionen. Nachr. Ges. Wiss. G\u00f6tt., Math.-Phys. Kl. 1899, 240\u2013242 (1899)","journal-title":"Nachr. Ges. Wiss. G\u00f6tt., Math.-Phys. Kl."},{"key":"843_CR36","first-page":"1","volume-title":"Proceedings of HSCC\u201917","author":"E. Goubault","year":"2017","unstructured":"Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Proceedings of HSCC\u201917, pp.\u00a01\u201310. ACM, New York (2017)"},{"key":"843_CR37","volume-title":"CAV","author":"E. Goubault","year":"2018","unstructured":"Goubault, E., Putot, S., Sahlmann, L.: Inner and Outer Approximating Flowpipes for Delay Differential Equations. In: CAV (2018)"},{"key":"843_CR38","volume-title":"CAV","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV (1997)"},{"key":"843_CR39","volume-title":"Concrete Mathematics","author":"R.L. Graham","year":"1989","unstructured":"Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics. Addison-Wesley, Reading (1989)"},{"key":"843_CR40","volume-title":"CAV","author":"I. Hasuo","year":"2012","unstructured":"Hasuo, I., Suenaga, K.: Exercises in nonstandard static analysis of hybrid systems. In: CAV (2012)"},{"key":"843_CR41","doi-asserted-by":"crossref","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. Comput. Program. 58(1\u20132) (2005)","DOI":"10.1016\/j.scico.2005.02.006"},{"issue":"4","key":"843_CR42","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/BF01208503","volume":"36","author":"D. Hilbert","year":"1890","unstructured":"Hilbert, D.: Ueber die Theorie der algebraischen Formen. Math. Ann. 36(4), 473\u2013534 (1890)","journal-title":"Math. Ann."},{"issue":"3","key":"843_CR43","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BF01444162","volume":"42","author":"D. Hilbert","year":"1893","unstructured":"Hilbert, D.: Ueber die vollen Invariantensysteme. Math. Ann. 42(3), 313\u2013373 (1893)","journal-title":"Math. Ann."},{"key":"843_CR44","unstructured":"Hoffmann, J.: Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis. Ph.D. thesis (2011). Advisor: Martin Hofmann"},{"key":"843_CR45","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis TOPLAS (2012)","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"843_CR46","volume-title":"AURA: Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty","author":"Z. Huang","year":"2025","unstructured":"Huang, Z., Laurel, J., Dutta, S., Misailovic, S.: AURA: Precise Abstract Interpretation of Probabilistic Programs with Interval Data Uncertainty. In: SAS (2025)"},{"key":"843_CR47","unstructured":"Hunt, S.: Abstract interpretation of functional languages: from theory to practice. Ph.D. thesis (1991). Advisor: Chris Hankin"},{"key":"843_CR48","volume-title":"OOPSLA","author":"K.J. Johnson","year":"2024","unstructured":"Johnson, K.J., Krishnan, R., Reps, T., D\u2019Antoni, L.: Automating pruning in top-down enumeration for program synthesis problems with monotonic semantics. In: OOPSLA (2024)"},{"key":"843_CR49","volume-title":"FOSSACS","author":"D.M. Kahn","year":"2020","unstructured":"Kahn, D.M., Hoffmann, J.: Exponential automatic amortized resource analysis. In: FOSSACS (2020)"},{"key":"843_CR50","volume-title":"OOPSLA","author":"P.K. Kalita","year":"2022","unstructured":"Kalita, P.K., Muduli, S.K., D\u2019Antoni, L., Reps, T., Roy, S.: Synthesizing abstract transformers. In: OOPSLA (2022)"},{"issue":"2","key":"843_CR51","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"},{"key":"843_CR52","first-page":"33","volume-title":"The Extended Interval Space IR","author":"E. Kaucher","year":"1980","unstructured":"Kaucher, E.: Interval analysis. In: The Extended Interval Space IR, pp.\u00a033\u201349. Springer, Vienna (1980)"},{"key":"843_CR53","volume-title":"Elementary Calculus: An Infinitesimal Approach","author":"H.J. Keisler","year":"2012","unstructured":"Keisler, H.J.: Elementary Calculus: An Infinitesimal Approach, 3rd edn. Dover, New York (2012). https:\/\/people.math.wisc.edu\/hkeisler\/calc.html","edition":"3"},{"key":"843_CR54","volume-title":"Basic Concepts of Enriched Category Theory","author":"M. Kelly","year":"1982","unstructured":"Kelly, M.: Basic Concepts of Enriched Category Theory. Cambridge University Press, Cambridge (1982)"},{"key":"843_CR55","volume-title":"Symbolic and Numerical Methods for Reachability Analysis","author":"K. Kido","year":"2015","unstructured":"Kido, K., Chaudhuri, S., Hasuo, I.: Abstract interpretation with infinitesimals: towards scalability in nonstandard static analysis. In: Symbolic and Numerical Methods for Reachability Analysis (2015)"},{"key":"843_CR56","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":"843_CR57","volume-title":"OOPSLA","author":"J. Laurel","year":"2023","unstructured":"Laurel, J., Qian, S.B., Singh, G., Misailovic, S.: Synthesizing precise static analyzers for automatic differentiation. In: OOPSLA (2023)"},{"key":"843_CR58","doi-asserted-by":"crossref","unstructured":"Le Metayer, D.: ACE: an Automatic Complexity Evaluator TOPLAS (1988)","DOI":"10.1145\/42190.42347"},{"key":"843_CR59","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, NY (2008)"},{"key":"843_CR60","volume-title":"FroCos","author":"N. Lommen","year":"2023","unstructured":"Lommen, N., Giesl, J.: Targeting completeness: using closed forms for size bounds of integer programs. In: FroCos (2023)"},{"key":"843_CR61","volume-title":"ICLP","author":"P. Lopez-Garcia","year":"2016","unstructured":"Lopez-Garcia, P., Klemen, M., Liqat, U., Hermenegildo, M.: A general framework for static profiling of parametric resource usage. In: ICLP (2016)"},{"key":"843_CR62","doi-asserted-by":"crossref","unstructured":"Lopez-Garcia, P., Darmawan, L., Klemen, M., Liqat, U., Bueno, F., Hermenegildo, M.: Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption. TPLP (2018)","DOI":"10.1017\/S1471068418000042"},{"key":"843_CR63","volume-title":"AST","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: AST (2001)"},{"key":"843_CR64","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: A New Numerical Abstract Domain Based on Difference-Bound Matrices (2001)","DOI":"10.1007\/3-540-44978-7_10"},{"key":"843_CR65","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages (2017)","DOI":"10.1561\/9781680833874"},{"key":"843_CR66","volume-title":"POPL","author":"D. Monniaux","year":"2009","unstructured":"Monniaux, D.: Automatic modular abstractions for linear constraints. In: POPL (2009)"},{"key":"843_CR67","volume-title":"CAV","author":"D. Monniaux","year":"2009","unstructured":"Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: CAV (2009)"},{"key":"843_CR68","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for template numerical constraints LMCS (2010)","DOI":"10.2168\/LMCS-6(3:4)2010"},{"key":"843_CR69","volume-title":"CAV","author":"D. Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier elimination by lazy model enumeration. In: CAV (2010)"},{"key":"843_CR70","volume-title":"ML Family Workshop","author":"B. Montagu","year":"2023","unstructured":"Montagu, B.: The design and implementation of an abstract interpreter for OCaml programs. In: ML Family Workshop (2023)"},{"key":"843_CR71","volume-title":"ICFP","author":"B. Montagu","year":"2020","unstructured":"Montagu, B., Jensen, T.: Stable relations and abstract interpretation of higher-order programs. In: ICFP (2020)"},{"issue":"5","key":"843_CR72","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/j.ipl.2004.05.004","volume":"91","author":"M. M\u00fcller-Olm","year":"2004","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Computing polynomial program invariants. Inf. Process. Lett. 91(5), 233\u2013244 (2004)","journal-title":"Inf. Process. Lett."},{"key":"843_CR73","volume-title":"ICLP","author":"J. Navas","year":"2007","unstructured":"Navas, J., Mera, E., Lopez-Garcia, P., Hermenegildo, M.: User-definable resource bounds analysis for logic programs. In: ICLP (2007)"},{"key":"843_CR74","volume-title":"CAV","author":"M. Oulamara","year":"2015","unstructured":"Oulamara, M., Venet, A.J.: Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation. In: CAV (2015)"},{"issue":"2","key":"843_CR75","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":"843_CR76","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-7091-1616-6_11","volume-title":"Computer Algebra in Quantum Field Theory: Integration, Summation and Special Functions","author":"M. Petkov\u0161ek","year":"2013","unstructured":"Petkov\u0161ek, M., Zakraj\u0161ek, H.: Solving linear recurrence equations with polynomial coefficients. In: Computer Algebra in Quantum Field Theory: Integration, Summation and Special Functions, pp.\u00a0259\u2013284. Springer, Berlin (2013)"},{"key":"843_CR77","doi-asserted-by":"crossref","unstructured":"Plotkin, G.: LCF considered as a programming language. Theoretical Computer Science (1977)","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"843_CR78","doi-asserted-by":"crossref","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. VMCAI (2004)","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"843_CR79","first-page":"3","volume-title":"All Concepts Are Kan Extensions","author":"E. Riehl","year":"2014","unstructured":"Riehl, E.: Categorical homotopy theory. In: All Concepts Are Kan Extensions, pp.\u00a03\u201316. Cambridge University Press, Cambridge (2014)"},{"key":"843_CR80","volume-title":"Non-standard Analysis","author":"A. Robinson","year":"1966","unstructured":"Robinson, A.: Non-standard Analysis. Princeton University Press, Princeton (1966)"},{"issue":"1","key":"843_CR81","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":"843_CR82","volume-title":"FPCA","author":"M. Rosendahl","year":"1989","unstructured":"Rosendahl, M.: Automatic complexity analysis. In: FPCA (1989)"},{"key":"843_CR83","doi-asserted-by":"crossref","unstructured":"Roux, P., Voronin, Y.L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants FMSD (2018)","DOI":"10.1007\/s10703-017-0302-y"},{"key":"843_CR84","unstructured":"Rustenholz, L.: Automated Approximate Recurrence Solving applied to Static Analysis of Energy Consumption. Tech. Rep. CLIP Lab, IMDEA Software Institute:. https:\/\/cliplab.org\/papers\/rustenholz-aars-msc.pdf (2022)"},{"issue":"6","key":"843_CR85","doi-asserted-by":"publisher","first-page":"1163","DOI":"10.1017\/S1471068424000413","volume":"24","author":"L. Rustenholz","year":"2024","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. Theory Pract. Log. Program. 24(6), 1163\u20131207 (2024). https:\/\/doi.org\/10.1017\/S1471068424000413","journal-title":"Theory Pract. Log. Program."},{"key":"843_CR86","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-74776-2_14","volume-title":"Proceedings of the 31st Static Analysis Symposium (SAS 2024)","author":"L. Rustenholz","year":"2024","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. In: Proceedings of the 31st Static Analysis Symposium (SAS 2024). LNCS, vol.\u00a014995. Springer, Berlin (2024). https:\/\/doi.org\/10.1007\/978-3-031-74776-2_14"},{"key":"843_CR87","volume-title":"An Order Theory Framework of Recurrence Equations for Static Cost Analysis - Dynamic Inference of Non-linear Inequality Invariants","author":"L. Rustenholz","year":"2024","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"},{"key":"843_CR88","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-01721-1","volume-title":"Modal Interval Analysis: New Tools for Numerical Information","author":"M.A. Sainz","year":"2014","unstructured":"Sainz, M.A., Armengol, J., Calm, R., Herrero, P., Jorba, L., Vehi, J.: Modal Interval Analysis: New Tools for Numerical Information. Springer, Berlin (2014)"},{"key":"843_CR89","volume-title":"VMCAI","author":"S. Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: VMCAI (2005)"},{"key":"843_CR90","volume-title":"Proc. International Conference on Algebraic and Logic Programming","author":"D.S. Scott","year":"1982","unstructured":"Scott, D.S.: Domains for denotational semantics. In: Proc. International Conference on Algebraic and Logic Programming. Springer, Berlin (1982)"},{"key":"843_CR91","volume-title":"ICLP","author":"A. Serrano","year":"2013","unstructured":"Serrano, A., Lopez-Garcia, P., Bueno, F., Hermenegildo, M.: Sized type analysis for logic programs. In: ICLP (2013)"},{"issue":"4\u20135","key":"843_CR92","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1017\/S147106841400057X","volume":"14","author":"A. Serrano","year":"2014","unstructured":"Serrano, A., Lopez-Garcia, P., Hermenegildo, M.: Resource usage analysis of logic programs via abstract interpretation using sized types. Theory Pract. Log. Program. 14(4\u20135), 739\u2013754 (2014)","journal-title":"Theory Pract. Log. Program."},{"key":"843_CR93","doi-asserted-by":"crossref","unstructured":"Shary, S.P.: Non-traditional intervals and their use. Which ones really make sense? Numer. Anal. Appl. (2023)","DOI":"10.1134\/S1995423923020088"},{"key":"843_CR94","unstructured":"Smith, P.: The Galois Connection between Syntax and Semantics. https:\/\/www.logicmatters.net\/resources\/pdfs\/Galois.pdf"},{"key":"843_CR95","unstructured":"Tanny, S.: An invitation to nested recurrence relations. Talk at CanaDAM (2013)"},{"key":"843_CR96","unstructured":"The Sage Developers: SageMath, the Sage Mathematics Software System (Version 10.2) (2024)"},{"key":"843_CR97","volume-title":"SAS","author":"C. Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: SAS (2014)"},{"key":"843_CR98","volume-title":"ECOOP","author":"M. Valnet","year":"2025","unstructured":"Valnet, M., Monat, R., Min\u00e9, A.: Compositional static value analysis for higher-order numerical programs. In: ECOOP (2025)"},{"key":"843_CR99","volume-title":"IFL","author":"P. Vasconcelos","year":"2003","unstructured":"Vasconcelos, P., Hammond, K.: Inferring cost equations for recursive, polymorphic and higher-order functional programs. In: IFL (2003)"},{"issue":"9","key":"843_CR100","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)","journal-title":"Commun. ACM"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00843-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-026-00843-3","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00843-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T14:04:03Z","timestamp":1781705043000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-026-00843-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,19]]},"references-count":100,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["843"],"URL":"https:\/\/doi.org\/10.1007\/s10009-026-00843-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,19]]},"assertion":[{"value":"20 February 2026","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 March 2026","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}