zbMATH — the first resource for mathematics

Tight polynomial worst-case bounds for loop programs. (English) Zbl 07215283
Summary: In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming language – representing non-deterministic imperative programs with bounded loops, and arithmetics limited to addition and multiplication – it is possible to decide precisely whether a program has certain growth-rate properties, in particular whether a computed value, or the program’s running time, has a polynomial growth rate.
A natural and intriguing problem was to move from answering the decision problem to giving a quantitative result, namely, a tight polynomial upper bound. This paper shows how to obtain asymptotically-tight, multivariate, disjunctive polynomial bounds for this class of programs. This is a complete solution: whenever a polynomial bound exists it will be found.
A pleasant surprise is that the algorithm is quite simple; but it relies on some subtle reasoning. An important ingredient in the proof is the forest factorization theorem, a strong structural result on homomorphisms into a finite monoid.
03B70 Logic in computer science
68 Computer science
Full Text: Link arXiv
[1] Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Radhia Cousot and Matthieu Martel, editors,Static Analysis Symposium, SAS’10, volume 6337 ofLNCS, pages · Zbl 1306.68017
[2] Amir M. Ben-Amram. On decidable growth-rate properties of imperative programs. In Patrick Baillot, editor,International Workshop on Developments in Implicit Computational complExity · Zbl 1354.68076
[3] Amir M. Ben-Amram and Samir Genaim. Ranking functions for linear-constraint loops.Journal of the ACM, 61(4):26:1-26:55, jul 2014. · Zbl 1321.68296
[4] Amir M. Ben-Amram and Lars Kristiansen. On the edge of decidability in complexity analysis of loop programs.International Journal on the Foundations of Computer Science, 23(7):1451-1464, 2012. · Zbl 1266.68091
[5] Amir M. Ben-Amram and Aviad Pineles. Flowchart programs, regular expressions, and decidability of polynomial growth-rate. In Geoff Hamilton, Alexei Lisitsa, and Andrei P. Nemytykh, editors, Proceedings of the Fourth International Workshop onVerification and Program Transfor
[6] Amir M. Ben-Amram and Samir Genaim. On multiphase-linear ranking functions. In Rupak Majumdar and Viktor Kuncak, editors,Computer Aided Verification, CAV’17, volume 10427 of · Zbl 1321.68296
[7] Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems.Sci. Comput. Program., 72(1-2):3-21, 2008. · Zbl 1138.68474
[8] Amir M. Ben-Amram, Neil D. Jones, and Lars Kristiansen. Linear, polynomial or exponential? complexity inference in polynomial time. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors,Logic and Theory of Algorithms, Fourth Conference on Computability in · Zbl 1142.68369
[9] Mikołaj Bojańczyk. Factorization forests. In Volker Diekert and Dirk Nowotka, editors,Developments in Language Theory, 13th International Conference, DLT 2009, Stuttgart, Germany, June 30 - July 3, 2009. Proceedings, volume 5583 ofLecture Notes in Computer Science, pages 1-17. · Zbl 1247.68127
[10] Thomas Colcombet, Laure Daviaud, and Florian Zuleger. Size-change abstraction and maxplus automata. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, · Zbl 1425.68190
[11] Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao. Compositional certified resource bounds. InProceedings of the ACM SIGPLAN 2015 Conference on Programming Language Design and
[12] Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. Polynomial invariants for affine programs. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer
[13] Lars Kristiansen James Avery and Jean-Yves Moyen. Static complexity analysis of higher order programs. InInternational Workshop on Foundational and Practical Aspects of Resource · Zbl 1305.68052
[14] Neil D. Jones and Lars Kristiansen. A flow calculus of mwp-bounds for complexity analysis. ACM Trans. Computational Logic, 10(4):1-41, 2009. · Zbl 1351.68075
[15] Raphaël M. Jungers, Vladimir Protasov, and Vincent D. Blondel. Efficient algorithms for deciding the type of growth of products of integer matrices.Linear Algebra and its Applications, 428:2296- 2311, 2008. · Zbl 1145.65030
[16] Takumi Kasai and Akeo Adachi. A characterization of time complexity by simple loop programs. Journal of Computer and System Sciences, 20(1):1-17, 1980. · Zbl 0431.03027
[17] Zachary Kincaid. Numerical invariants via abstract machines. In A. Podelski, editor,Static Analysis—25th International Symposium, SAS 2018, Proceedings, volume 11002 ofLNCS, pages
[18] Lars Kristiansen and Karl-Heinz Niggl. On the computational complexity of imperative programming languages.Theor. Comp. Sci., 318(1-2):139-161, 2004. · Zbl 1048.03030
[19] Daniel Le Métayer. Ace: an automatic complexity evaluator.ACM Trans. Program. Lang. Syst., 10(2):248-266, 1988.
[20] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. InProc. 28th ACM Symp. on Principles of Programming Languages, 81-92. ACM press, 2001. · Zbl 1323.68216
[21] Richard Mayr. Undecidable problems in unreliable computations.Theor. Comput. Sci, 297(13):337-354, 2003. · Zbl 1044.68119
[22] Kenneth L. McMillan and Oded Padon. Deductive verification in decidable fragments with ivy. In A. Podelski, editor,Static Analysis—25th International Symposium, SAS 2018, Proceedings, volume 11002 ofLNCS, pages 43-55. Springer, 2018.
[23] Markus Müller-Olm and Helmut Seidl. Computing polynomial program invariants.Information Processing Letters, 91(5):233-244, 2004. · Zbl 1177.68048
[24] Albert R. Meyer and Dennis M. Ritchie. The complexity of loop programs. InProc. 22nd ACM National Conference, pages 465-469, Washington, DC, 1967.
[25] Karl-Heinz Niggl and Henning Wunderlich. Certifying polynomial time and linear/polynomial space for imperative programs.SIAM J. Comput, 35(5):1122-1147, 2006. · Zbl 1100.68035
[26] Andreas Podelski and Andrey Rybalchenko. A complete method for synthesis of linear ranking functions. In Bernhard Steffen and Giorgio Levi, editors,VMCAI 2003: Verification, Model · Zbl 1202.68109
[27] M. Rosendahl. Automatic complexity analysis. InProceedings of the Conference on Functional Programming Languages and Computer Architecture FPCA’89, pages 144-156. ACM, 1989.
[28] Imre Simon. Factorization forests of finite height.Theoretical Computer Science, 72(1):65-94, 1990. · Zbl 0693.68044
[29] Moritz Sinn, Florian Zuleger, and Helmut Veith. Complexity and resource bound analysis of imperative programs using difference constraints.Journal of Automated Reasoning, 59(1):3-45, 2017. · Zbl 1409.68076
[30] Ben Wegbreit. Mechanical program analysis.Communications of the ACM, 18(9):528-539, 1975. · Zbl 0306.68008
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.