Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants

  • Conference paper
  • First Online:
Static Analysis(SAS 2024)

Abstract

Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtainnon-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours.

This work has been partially supported by the Tezos foundation and by MICINN projects PID2019-108528RB-C21ProCode and TED2021-132464B-I00PRODIGY.

This is a preview of subscription content,log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 8464
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 10581
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide -see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Notes

  1. 1.

    We refer the interested reader to the extended version of this paper [58] (discussing, e.g., unbounded optimisation for non-deterministic equations, and self-composition) or to our future work, where we plan to expose such theory in more detail.

  2. 2.

    This (interprocedural abstract interpretation by polyhedra+disjunctions to obtain affine bounds, if possible, on solutions of equations represented as programs) can be considered “folklore”, but we are not aware of full descriptions in the literature.

References

  1. Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason.46(2), 161–203 (2011)

    Article MathSciNet MATH  Google Scholar 

  2. Albert, E., Correas, J., Gordillo, P., Román-Díez, G., Rubio, A.: GASOL: gas analysis and optimization for ethereum smart contracts. In: TACAS 2020. LNCS, vol. 12079, pp. 118–125. Springer, Cham (2020).https://doi.org/10.1007/978-3-030-45237-7_7

    Chapter MATH  Google Scholar 

  3. Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., Stankovič, M.: (Un)Solvable loop analysis. arXiv2306.01597 (2023)

    Google Scholar 

  4. Andersen, M.S., Dahl, J., Vandenberghe, L.: CVXOPT: a python package for convex optimization, version 1.3.2 (2023), available athttps://cvxopt.org/

  5. Applegate, D.L., Cook, W., Dash, S., Espinoza, D.G.: Exact solutions to linear programming problems. Oper. Res. Lett.35(6), 693–699 (2007)

    Article MathSciNet MATH  Google Scholar 

  6. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds.) FMP &TA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993).https://doi.org/10.1007/BFb0039704

    Chapter MATH  Google Scholar 

  7. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979, pp. 269–282. ACM (1979)

    Google Scholar 

  8. Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)

    MATH  Google Scholar 

  9. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (2002)

    Book MATH  Google Scholar 

  10. Debray, S.K., Lin, N.W.: Cost analysis of logic programs. TOPLAS (1993)

    Google Scholar 

  11. Debray, S.K., Lin, N.W., Hermenegildo, M.V.: Task granularity analysis in logic programs. In: Proceedings of PLDI 1990, pp. 174–188. ACM (1990)

    Google Scholar 

  12. Debray, S.K., Lopez-Garcia, P., Hermenegildo, M.V., Lin, N.W.: Lower bound cost estimation for logic programs. In: ILPS 1997, pp. 291–305. MIT Press (1997)

    Google Scholar 

  13. Doménech, J.J., Gallagher, J.P., Genaim, S.: Control-flow refinement by partial evaluation, and its application to termination and cost analysis. TPLP (2019)

    Google Scholar 

  14. Ernst, M., Cockrell, J., Griswold, W., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw, Eng (2001)

    Google Scholar 

  15. Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004).https://doi.org/10.1007/978-3-540-24725-8_4

    Chapter MATH  Google Scholar 

  16. Feret, J.: The arithmetic-geometric progression abstract domain. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 42–58. Springer, Heidelberg (2005).https://doi.org/10.1007/978-3-540-30579-8_3

    Chapter MATH  Google Scholar 

  17. Flajolet, P., Sedgewick, R.: Analytic Combinatorics. CUP (2009)

    Google Scholar 

  18. Flores-Montoya, A.: Cost Analysis of Programs Based on the Refinement of Cost Relations. Ph.D. thesis, T.U. Darmstadt (2017). Advisor: Reiner Hähnle

    Google Scholar 

  19. Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) IJCAR 2022. LNCS, vol. 13385, pp. 712–722. Springer, Cham (2022).https://doi.org/10.1007/978-3-031-10769-6_41

    Chapter MATH  Google Scholar 

  20. 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–228. Springer, Cham (2022).https://doi.org/10.1007/978-3-031-08166-8_10

  21. 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–166. Springer, Cham (2019).https://doi.org/10.1007/978-3-030-17502-3_10

    Chapter MATH  Google Scholar 

  22. Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Proceedings of HSCC 2017, pp. 1–10. ACM (2017)

    Google Scholar 

  23. 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–541. Springer, Cham (2018).https://doi.org/10.1007/978-3-319-96142-2_31

    Chapter MATH  Google Scholar 

  24. Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics. Addison-Wesley, Hoboken (1989)

    MATH  Google Scholar 

  25. Hastie, T., Tibshirani, R., Wainwright, M.: Statistical Learning with Sparsity: The Lasso and Generalizations. Chapman & Hall/CRC (2015)

    Google Scholar 

  26. 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–2), 115–140 (2005)

    Article MathSciNet MATH  Google Scholar 

  27. Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM TOPLAS34(3), 14:1–14:62 (2012)

    Google Scholar 

  28. Humenberger, A., Jaroschek, M., Kovács, L.: Automated generation of non-linear loop invariants utilizing hypergeometric sequences, pp. 221–228. ISSAC 2017 (2017)

    Google Scholar 

  29. Ishimwe, D., Nguyen, K., Nguyen, T.: Dynaplex: analyzing program complexity using dynamically inferred recurrence relations. In: OOPSLA (2021)

    Google Scholar 

  30. Karp, R.: Probabilistic recurrence relations. J. ACM41(6), 1136–1150 (1994)

    Article MathSciNet MATH  Google Scholar 

  31. Karr, M.: Summation in finite terms. J. ACM28(2), 305–350 (1981)

    Article MathSciNet MATH  Google Scholar 

  32. Kimberling, C.: Best lower and upper approximates to irrational numbers. Elem. Math.52(3), 122–126 (1997)

    Article MathSciNet MATH  Google Scholar 

  33. Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. POPL (2018)

    Google Scholar 

  34. Knaster, B.: Un théorème sur les fonctions d’ensembles. Ann. Soc. Polon. Math.6, 133–134 (1928), with A. Tarski

    Google Scholar 

  35. Kovács, 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

    Google Scholar 

  36. Lang, S.: Introduction to Diophantine Approximations, 2nd edn. Springer, New York (1995)

    Book MATH  Google Scholar 

  37. Le Metayer, D.: ACE: an automatic complexity evaluator. TOPLAS (1988)

    Google Scholar 

  38. Levin, A.: Difference Algebra Algebra and Applications. Springer, New York (2008)

    Book MATH  Google Scholar 

  39. 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–22. Springer, Cham (2023).https://doi.org/10.1007/978-3-031-43369-6_1

    Chapter MATH  Google Scholar 

  40. 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. TPLP18(2), 167–223 (2018)

    MathSciNet MATH  Google Scholar 

  41. Lopez-Garcia, P., Klemen, M., Liqat, U., Hermenegildo, M.V.: A general framework for static profiling of parametric resource usage. In: ICLP (2016)

    Google Scholar 

  42. Lv, M., Guan, N., Reineke, J., Wilhelm, R., Yi, W.: A survey on static cache analysis for real-time systems. LITES3(1), 05:1–05:48 (2016)

    Google Scholar 

  43. Wolfram Mathematica (v13.2): The World’s Definitive System for Modern Technical Computing.https://www.wolfram.com/mathematica. Accessed 25 May 2023

  44. 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–583. Springer, Heidelberg (2009).https://doi.org/10.1007/978-3-642-02658-4_42

    Chapter MATH  Google Scholar 

  45. Navas, J., Mera, E., López-García, P., Hermenegildo, M.V.: User-definable resource bounds analysis for logic programs. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 348–363. Springer, Heidelberg (2007).https://doi.org/10.1007/978-3-540-74610-2_24

    Chapter MATH  Google Scholar 

  46. Nedialkov, N., Jackson, K., Corliss, G.: Validated solutions of initial value problems for ordinary differential equations. Appl. Math. Comput.105(1), 21–68 (1999)

    MathSciNet MATH  Google Scholar 

  47. Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: ICSE (2012)

    Google Scholar 

  48. Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to generate disjunctive invariants. In: ICSE (2014)

    Google Scholar 

  49. Nguyen, T., Nguyen, K., Dwyer, M.B.: Using symbolic states to infer numerical invariants. IEEE Trans. Software Eng.48(10), 3877–3899 (2022)

    Article MATH  Google Scholar 

  50. Pérez, V., Klemen, M., López-García, 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–31. Springer, Cham (2020).https://doi.org/10.1007/978-3-030-65474-0_2

    Chapter MATH  Google Scholar 

  51. Petkovšek, M.: Hypergeometric solutions of linear recurrences with polynomial coefficients. J. Symb. Comput.14(2), 243–264 (1992)

    Article MathSciNet MATH  Google Scholar 

  52. Petkovšek, M., Zakrajšek, H.: Solving linear recurrence equations with polynomial coefficients. In: Schneider, C., Blümlein, J. (eds) Computer Algebra in Quantum Field Theory: Integration, Summation and Special Functions, pp. 259–284. Springer, Vienna (2013).https://doi.org/10.1007/978-3-7091-1616-6_11

  53. Pham, L., Saad, F.A., Hoffmann, J.: Robust resource bounds with static analysis and Bayesian inference. In: PLDI (2024)

    Google Scholar 

  54. Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program.64(1), 54–75 (2007). Special issue on SAS 2004

    Article MathSciNet MATH  Google Scholar 

  55. Rosendahl, M.: Automatic complexity analysis. In: FPCA (1989)

    Google Scholar 

  56. 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

  57. Rustenholz, L., Klemen, M., Carreira-Perpiñán, M.Á., López-García, 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

  58. 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)

  59. Rustenholz, L., Lopez-Garcia, P., Morales, J.F., Hermenegildo, M.: Artifact for “an order theory framework of recurrence equations for static cost analysis – dynamic inference of non-linear inequality invariants” (2024).https://doi.org/10.5281/zenodo.13133801

  60. Serrano, A., Lopez-Garcia, P., Hermenegildo, M.V.: Resource usage analysis of logic programs via abstract interpretation using sized types. ICLP (2014)

    Google Scholar 

  61. Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason.59(1), 3–45 (2017)

    Article MathSciNet MATH  Google Scholar 

  62. Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput.11(4), 761–783 (1982)

    Article MathSciNet MATH  Google Scholar 

  63. 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–39. Springer, Cham (2023).https://doi.org/10.1007/978-3-031-37709-9_2

    Chapter  Google Scholar 

  64. Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math.5(2), 285–309 (1955)

    Article MathSciNet MATH  Google Scholar 

  65. Wang, C., Lin, F.: Solving conditional linear recurrences for program verification: the periodic case. Proc. ACM Program. Lang.7(OOPSLA1), 28–55 (2023)

    Article MATH  Google Scholar 

  66. Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: PLDI (2021)

    Google Scholar 

  67. Wegbreit, B.: Mechanical program analysis. Commun. ACM18(9), 528–539 (1975).https://doi.org/10.1145/361002.361016

    Article MathSciNet MATH  Google Scholar 

  68. Westrick, S., Fluet, M., Rainey, M., Acar, U.A.: Automatic parallelism management. In: POPL (2024)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidad Politécnica de Madrid (UPM), Madrid, Spain

    Louis Rustenholz, José F. Morales & Manuel V. Hermenegildo

  2. Spanish Council for Scientific Research (CSIC), Madrid, Spain

    Pedro López-García

  3. IMDEA Software Institute, Pozuelo de Alarcon, Spain

    Louis Rustenholz, Pedro López-García, José F. Morales & Manuel V. Hermenegildo

Authors
  1. Louis Rustenholz

    You can also search for this author inPubMed Google Scholar

  2. Pedro López-García

    You can also search for this author inPubMed Google Scholar

  3. José F. Morales

    You can also search for this author inPubMed Google Scholar

  4. Manuel V. Hermenegildo

    You can also search for this author inPubMed Google Scholar

Corresponding author

Correspondence toLouis Rustenholz.

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Arizona, Tucson, AZ, USA

    Roberto Giacobazzi

  2. IMDEA Software Institute, Pozuelo de Alarcon, Madrid, Spain

    Alessandra Gorla

Ethics declarations

Disclosure of Interests

The authors have no competing interests to declare that are relevant to the content of this article.

A Tables of Experimental Data

A Tables of Experimental Data

Table 2. Benchmarks
figure a
Table 3. Full results obtained by each tool for the running example. Results for the symbolic regression presented in [57] is included for completeness: it does not manage to discover the exact solution either, even if floor and division nodes are allowed.

Rights and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Rustenholz, L., López-García, P., Morales, J.F., Hermenegildo, M.V. (2025). An Order Theory Framework of Recurrence Equations for Static Cost Analysis – Dynamic Inference of Non-Linear Inequality Invariants. In: Giacobazzi, R., Gorla, A. (eds) Static Analysis. SAS 2024. Lecture Notes in Computer Science, vol 14995. Springer, Cham. https://doi.org/10.1007/978-3-031-74776-2_14

Download citation

Publish with us

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 8464
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 10581
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide -see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

[8]ページ先頭
©2009-2025 Movatter.jp