Krishnendu Chatterjee
Skip Abstract Section
Abstract
We study the problem of developing efficient approaches for proving worst-case bounds of non-deterministic recursive programs. Ranking functions are sound and complete for proving termination and worst-case bounds of non-recursive programs. First, we apply ranking functions to recursion, resulting in measure functions. We show that measure functions provide a sound and complete approach to prove worst-case bounds of non-deterministic recursive programs. Our second contribution is the synthesis of measure functions in non-polynomial forms. We show that non-polynomial measure functions with logarithm and exponentiation can be synthesized through abstraction of logarithmic or exponentiation terms, Farkas Lemma, and Handelman’s Theorem using linear programming. While previous methods obtain polynomial worst-case bounds, our approach can synthesize bounds of various forms including O(n log n) and O(nr), where r is not an integer. We present experimental results to demonstrate that our approach can efficiently obtain worst-case bounds of classical recursive algorithms such as (i) Merge sort, Heap sort, and the divide-and-conquer algorithm for the Closest Pair problem, where we obtain O(n log n) worst-case bound, and (ii) Karatsuba’s algorithm for polynomial multiplication and Strassen’s algorithm for matrix multiplication, for which we obtain O(nr) bounds such that r is not an integer and is close to the best-known bound for the respective algorithm. Besides the ability to synthesize non-polynomial bounds, we also show that our approach is equally capable of obtaining polynomial worst-case bounds for classical programs such as Quick sort and the dynamic programming algorithm for computing Fibonacci numbers.
- Elvira Albert, Puri Arenas, Samir Genaim, Miguel Gómez-Zamalloa, German Puebla, Diana V. Ramírez-Deantes, Guillermo Román-Díez, and Damiano Zanardini. 2009. Termination and cost analysis with COSTA and its user interfaces. Electr. Notes Theor. Comput. Sci. 258, 1 (2009), 109–121. DOI:https://doi.org/10.1016/j.entcs.2009.12.008Google Scholar
Digital Library
- Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. 2008. Automatic inference of upper bounds for recurrence relations in cost analysis. In Proceedings of the 15th International Symposium on Static Analysis (SAS’08), (Lecture Notes in Computer Science), María Alpuente and Germán Vidal (Eds.). Vol. 5079, Springer, 221--237. DOI:https://doi.org/10.1007/978-3-540-69166-2_15Google ScholarDigital Library
- Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla, and Damiano Zanardini. 2007. Cost analysis of Java bytecode. In Programming Languages and Systems, 16th European Symposium on Programming (ESOP’07), held as part of the Proceedings of the Joint European Conferences on Theory and Practics of Software (ETAPS’07), (Lecture Notes in Computer Science), Rocco De Nicola (Ed.), Vol. 4421. Springer, 157--172. DOI:https://doi.org/10.1007/978-3-540-71316-6_12Google ScholarCross Ref
- Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of the Static Analysis Symposium (SAS’10), (LNCS), Radhia Cousot and Matthieu Martel (Eds.). Vol. 6337, Springer, 117--133. DOI:https://doi.org/10.1007/978-3-642-15769-1_8Google ScholarCross Ref
- Rajeev Alur and Swarat Chaudhuri. 2010. Temporal reasoning for procedural programs. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’10), (Lecture Notes in Computer Science), Gilles Barthe and Manuel V. Hermenegildo (Eds.), Vol. 5944. Springer, 45--60. DOI:https://doi.org/10.1007/978-3-642-11319-2_7Google ScholarDigital Library
- Roberto Bagnara, Patricia M Hill, Elisa Ricci, and Enea Zaffanella. 2003. Precise widening operators for convex polyhedra. In Proceedings of the International Static Analysis Symposium. Springer, 337--354.Google ScholarCross Ref
- Robert G. Bartle and Donald R. Sherbert. 2011. Introduction to Real Analysis (4th ed.). John Wiley 8 Sons, Inc.Google Scholar
- Rastislav Bodík and Rupak Majumdar (Eds.). 2016. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’16). ACM.Google ScholarDigital Library
- Olivier Bournez and Florent Garnier. 2005. Proving positive almost-sure termination. In 16th International Conference on Term Rewriting and Applications (RTA'05). Lecture Notes in Computer Science, Vol. 3467. Springer, 323--337.Google ScholarDigital Library
- Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear ranking with reachability. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05), (Lecture Notes in Computer Science), Kousha Etessami and Sriram K. Rajamani (Eds.), Vol. 3576. Springer, 491--504. DOI:https://doi.org/10.1007/11513988_48Google ScholarDigital Library
- Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and Jürgen Giesl. 2016. Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38, 4 (2016), 13:1--13:50. http://dl.acm.org/citation.cfm?id=2866575.Google ScholarDigital Library
- Giuseppe Castagna and Andrew D. Gordon (Eds.). 2017. Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). ACM. DOI:https://doi.org/10.1145/3009837Google ScholarDigital Library
- Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13), (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.). Vol. 8044, Springer, 511--526. DOI:https://doi.org/10.1007/978-3-642-39799-8_34Google ScholarCross Ref
- Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination analysis of probabilistic programs through Positivstellensatz’s. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV’16), Part I Lecture Notes in Computer Science, Swarat Chaudhuri and Azadeh Farzan (Eds.). Vol. 9779, Springer, 3--22. DOI:https://doi.org/10.1007/978-3-319-41528-4_1Google ScholarCross Ref
- Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2017. Non-polynomial worst-case analysis of recursive programs. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV’17), Part II, Lecture Notes in Computer Science, Rupak Majumdar and Viktor Kuncak (Eds.). Vol. 10427, Springer, 41--63.Google ScholarCross Ref
- Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. 2019. Polynomial invariant generation for non-deterministic recursive programs. CoRR abs/1902.04373 (2019). arxiv:1902.04373 http://arxiv.org/abs/1902.04373.Google Scholar
- Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs, See Reference Bodík and Majumdar [8], 327--342. DOI:https://doi.org/10.1145/2837614.2837639Google ScholarDigital Library
- Krishnendu Chatterjee, Petr Novotný, and Đorđe Žikelić. 2017. Stochastic invariants for probabilistic termination, See Reference Castagna and Gordon [12], 145--160. DOI:https://doi.org/10.1145/3009837Google ScholarDigital Library
- Wei-Ngan Chin and Siau-Cheng Khoo. 2001. Calculating sized types. Higher-Order. Comput. 14, 2--3 (2001), 261--300. DOI:https://doi.org/10.1023/A:1012996816178Google ScholarDigital Library
- Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. 2003. Linear invariant generation using non-linear constraint solving. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), Lecture Notes in Computer Science, Warren A. Hunt Jr. and Fabio Somenzi (Eds.). Vol. 2725, Springer, 420--432. DOI:https://doi.org/10.1007/978-3-540-45069-6_39Google ScholarCross Ref
- Michael Colón and Henny Sipma. 2001. Synthesis of linear ranking functions. In Proceedings of the 7th International ConferenceTools and Algorithms for the Construction and Analysis of Systems (TACAS’01), held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS’01), Lecture Notes in Computer Science, Tiziana Margaria and Wang Yi (Eds.). Vol. 2031, Springer, 67--81. DOI:https://doi.org/10.1007/3-540-45319-9_6Google ScholarCross Ref
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In Proceedings of the Programming Language Design and Implementation Conference (PLDI’06), Michael I. Schwartzbach and Thomas Ball (Eds.). ACM, 415--426. DOI:https://doi.org/10.1145/1133981.1134029Google ScholarDigital Library
- Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2009. Summarization for termination: No return! Formal Methods Syst. Des. 35, 3 (2009), 369--387. DOI:https://doi.org/10.1007/s10703-009-0087-8Google ScholarDigital Library
- Byron Cook, Abigail See, and Florian Zuleger. 2013. Ramsey vs. Lexicographic termination proving. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13), Lecture Notes in Computer Science, Nir Piterman and Scott A. Smolka (Eds.). Vol. 7795, Springer, 47--61. DOI:https://doi.org/10.1007/978-3-642-36742-7_4Google ScholarDigital Library
- Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). MIT Press.Google ScholarDigital Library
- Patrick Cousot. 2005. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’05), Lecture Notes in Computer Science, Radhia Cousot (Ed.). Vol. 3385, Springer, 1--24. DOI:https://doi.org/10.1007/978-3-540-30579-8_1Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238--252. DOI:https://doi.org/10.1145/512950.512973Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. 2012. An abstract interpretation framework for termination. In Proceedings of the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’12), John Field and Michael Hicks (Eds.). ACM, 245--258. DOI:https://doi.org/10.1145/2103656.2103687Google ScholarDigital Library
- J. Farkas. 1894. A Fourier-féle mechanikai elv alkalmazásai (Hungarian). Math. Term. Értesitö 12 (1894), 457--472.Google Scholar
- Luis María Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic termination: Soundness, completeness, and compositionality. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’15), Sriram K. Rajamani and David Walker (Eds.). ACM, 489--501. DOI:https://doi.org/10.1145/2676726.2677001Google ScholarDigital Library
- Philippe Flajolet, Bruno Salvy, and Paul Zimmermann. 1991. Automatic average-case analysis of algorithm. Theor. Comput. Sci. 79, 1 (1991), 37--109. DOI:https://doi.org/10.1016/0304-3975(91)90145-RGoogle ScholarDigital Library
- Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical Aspects of Computer Science (Proceedings of a Symposium in Applied Mathematics), J. T. Schwarz (Ed.) 19 (1967), 19--32.Google Scholar
- Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of nondeterministic probabilistic programs. In Proceedings of the 20th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’19), Lecture Notes in Computer Science, Constantin Enea and Ruzica Piskac (Eds.). Vol. 11388, Springer, 468--490. DOI:https://doi.org/10.1007/978-3-030-11245-5_22Google ScholarCross Ref
- Stéphane Gimenez and Georg Moser. 2016. The complexity of interaction, See Reference Bodík and Majumdar [8], 243--255. DOI:https://doi.org/10.1145/2837614.2837646Google ScholarDigital Library
- Kurt Gödel. On undecidable propositions of formal mathematical systems. 1934. A reprint of XXXI 484. The Journal of Symbolic Logic 55, 1 (1934), 347. https://doi.org/10.2307/2274987Google ScholarCross Ref
- Bernd Grobauer. 2001. Cost recurrences for DML programs. In Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming (ICFP’01), Benjamin C. Pierce (Ed.). ACM, 253--264. DOI:https://doi.org/10.1145/507635.507666Google ScholarDigital Library
- Bhargav S. Gulavani and Sumit Gulwani. 2008. A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV’08), Lecture Notes in Computer Science, Aarti Gupta and Sharad Malik (Eds.). Vol. 5123, Springer, 370--384. DOI:https://doi.org/10.1007/978-3-540-70545-1_35Google ScholarDigital Library
- Sumit Gulwani. 2009. SPEED: Symbolic complexity bound analysis. In Proceedings of the 21st International Conference on Computer Aided Verification, (CAV’09), Lecture Notes in Computer Science, Ahmed Bouajjani and Oded Maler (Eds.). Vol. 5643, Springer, 51--62. DOI:https://doi.org/10.1007/978-3-642-02658-4_7Google ScholarDigital Library
- Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: Precise and efficient static estimation of program computational complexity. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09), Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 127--139. DOI:https://doi.org/10.1145/1480881.1480898Google ScholarDigital Library
- D. Handelman. 1988. Representing polynomials by positive linear functions on compact convex polyhedra. Pac. J. Math. 132 (1988), 35--62.Google ScholarCross Ref
- Wim H. Hesselink. 1993. Proof rules for recursive procedures. Form. Asp. Comput. 5, 6 (1993), 554--570. DOI:https://doi.org/10.1007/BF01211249Google ScholarDigital Library
- Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34, 3 (2012), 14. DOI:https://doi.org/10.1145/2362389.2362393Google ScholarDigital Library
- Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012. Resource aware ML. In Proceedings of the 24th International Conference on Computer Aided Verification (CAV’12), Lecture Notes in Computer Science, P. Madhusudan and Sanjit A. Seshia (Eds.). Vol. 7358, Springer, 781--786. DOI:https://doi.org/10.1007/978-3-642-31424-7_64Google ScholarDigital Library
- Jan Hoffmann and Martin Hofmann. 2010. Amortized resource analysis with polymorphic recursion and partial big-step operational semantics. In Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS’10), Lecture Notes in Computer Science, Kazunori Ueda (Ed.). Vol. 6461, Springer, 172--187. DOI:https://doi.org/10.1007/978-3-642-17164-2_13Google ScholarCross Ref
- Jan Hoffmann and Martin Hofmann. 2010. Amortized resource analysis with polynomial potential. In Proceedings of the 19th European Symposium on Programming Languages and Systems (ESOP’10), held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS’10), Lecture Notes in Computer Science, Andrew D. Gordon (Ed.). Vol. 6012, Springer, 287--306. DOI:https://doi.org/10.1007/978-3-642-11957-6_16Google ScholarDigital Library
- Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In Conference Record of POPL 2003: Proceedings of the 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Alex Aiken and Greg Morrisett (Eds.). ACM, 185--197. DOI:https://doi.org/10.1145/640128.604148Google ScholarDigital Library
- Martin Hofmann and Steffen Jost. 2006. Type-based amortised heap-space analysis. In Proceedings of the 15th European Symposium on Programming Languages and Systems (ESOP’06) held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS’06), Lecture Notes in Computer Science, Peter Sestoft (Ed.). Vol. 3924, Springer, 22--37. DOI:https://doi.org/10.1007/11693024_3Google ScholarDigital Library
- Martin Hofmann and Dulma Rodriguez. 2009. Efficient type-checking for amortised heap-space analysis. In Proceedings of the 23rd International Workshop on the Conference on Computer Science Logic (CSL’09), Lecture Notes in Computer Science, Erich Grädel and Reinhard Kahle (Eds.). Vol. 5771, Springer, 317--331. DOI:https://doi.org/10.1007/978-3-642-04027-6_24Google ScholarCross Ref
- John Hughes and Lars Pareto. 1999. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In Proceedings of the 4th ACM SIGPLAN International Conference on Functional Programming (ICFP’99), Didier Rémi and Peter Lee (Eds.). ACM, 70--81. DOI:https://doi.org/10.1145/317636.317785Google ScholarDigital Library
- John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the correctness of reactive systems using sized types. In Conference Record of POPL’96: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Hans-Juergen Boehm and Guy L. Steele Jr. (Eds.). ACM Press, 410--423. DOI:https://doi.org/10.1145/237721.240882Google ScholarDigital Library
- Claire Jones. 1989. Probabilistic Non-Determinism. Ph.D. Dissertation. The University of Edinburgh.Google Scholar
- Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, and Martin Hofmann. 2010. Static determination of quantitative resource usage for higher-order programs. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’10), Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 223--236. DOI:https://doi.org/10.1145/1706299.1706327Google ScholarDigital Library
- Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, and Martin Hofmann. 2009. “Carbon credits” for resource-bounded computations using amortised analysis. In Proceedings of the Internaional Conference on Formal Methods (FM’09), Lecture Notes in Computer Science, Ana Cavalcanti and Dennis Dams (Eds.). Vol. 5850, Springer, 354--369. DOI:https://doi.org/10.1007/978-3-642-05089-3_23Google ScholarDigital Library
- Donald E. Knuth. 1973. The Art of Computer Programming, Volume I--III. Addison-Wesley.Google ScholarDigital Library
- Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi. 2014. Automatic termination verification for higher-order functional programs. In Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP'14). Lecture Notes in Computer Science, Vol. 8410, Zhong Shao (Ed.). Springer, 392--411. DOI:https://doi.org/10.1007/978-3-642-54833-8_21Google ScholarDigital Library
- Chin Soon Lee. 2009. Ranking functions for size-change termination. ACM Trans. Program. Lang. Syst. 31, 3 (2009), 10:1--10:42. DOI:https://doi.org/10.1145/1498926.1498928Google ScholarDigital Library
- Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In Proceedings of the Principles of Programming Languages Symposium (POPL’01), Chris Hankin and Dave Schmidt (Eds.). ACM, 81--92. DOI:https://doi.org/10.1145/360204.360210Google ScholarDigital Library
- lpsolve 2016. lp_solve 5.5.2.3. Retrieved from http://lpsolve.sourceforge.net/5.5/.Google Scholar
- Martin Lukasiewycz. 2008. Java ILP—Java Interface to ILP Solvers. Retrieved from http://javailp.sourceforge.net/.Google Scholar
- Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about recursive probabilistic programs. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’16), Martin Grohe, Eric Koskinen, and Natarajan Shankar (Eds.). ACM, 672--681. DOI:https://doi.org/10.1145/2933575.2935317Google ScholarDigital Library
- Andreas Podelski and Andrey Rybalchenko. 2004. A complete method for the synthesis of linear ranking functions. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation, (VMCAI’04), Lecture Notes in Computer Science, Bernhard Steffen and Giorgio Levi (Eds.). Vol. 2937, Springer, 239--251. DOI:https://doi.org/10.1007/978-3-540-24622-0_20Google ScholarCross Ref
- Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. 2004. Constraint-based linear-relations analysis. In International Static Analysis Symposium. Springer, 53--68.Google ScholarCross Ref
- Alexander Schrijver. 1999. Theory of Linear and Integer Programming. Wiley.Google ScholarDigital Library
- Alexander Schrijver. 2003. Combinatorial Optimization—Polyhedra and Efficiency. Springer.Google Scholar
- Liyong Shen, Min Wu, Zhengfeng Yang, and Zhenbing Zeng. 2013. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method. J. Syst. Sci. 8 Complexity 26, 2 (2013), 291--301. DOI:https://doi.org/10.1007/s11424-013-1004-1Google ScholarCross Ref
- Olha Shkaravska, Ron van Kesteren, and Marko C. J. D. van Eekelen. 2007. Polynomial size analysis of first-order functions. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications (TLCA’07), Lecture Notes in Computer Science, Simona Ronchi Della Rocca (Ed.). Vol. 4583, Springer, 351--365. DOI:https://doi.org/10.1007/978-3-540-73228-0_25Google ScholarCross Ref
- Moritz Sinn, Florian Zuleger, and Helmut Veith. 2014. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proceedings of the International Conference on Computer-aided Verification (CAV’14), Lecture Notes in Computer Science, Armin Biere and Roderick Bloem (Eds.). Vol. 8559, Springer, 745--761. DOI:https://doi.org/10.1007/978-3-319-08867-9_50Google ScholarDigital Library
- Kirack Sohn and Allen Van Gelder. 1991. Termination detection in logic programs using argument sizes. In Proceedings of the 10th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, Daniel J. Rosenkrantz (Ed.). ACM Press, 216--226. DOI:https://doi.org/10.1145/113413.113433Google ScholarDigital Library
- Akhilesh Srikanth, Burak Sahin, and William R. Harris. 2017. Complexity verification using guided theorem enumeration, See Reference Castagna and Gordon [12], 639--652. DOI:https://doi.org/10.1145/3009837Google ScholarDigital Library
- Caterina Urban. 2013. The abstract domain of segmented ranking functions. In Proceedings of the Static Analysis Symposium (SAS’13), Lecture Notes in Computer Science, Francesco Logozzo and Manuel Fähndrich (Eds.). Vol. 7935, Springer, 43--62. DOI:https://doi.org/10.1007/978-3-642-38856-9_5Google ScholarCross Ref
- Reinhard Wilhelm, Jakob Engblom, Andreas Ermedahl, Niklas Holsti, Stephan Thesing, David B. Whalley, Guillem Bernat, Christian Ferdinand, Reinhold Heckmann, Tulika Mitra, Frank Mueller, Isabelle Puaut, Peter P. Puschner, Jan Staschulat, and Per Stenström. 2008. The worst-case execution-time problem—Overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7, 3 (2008), 36:1--36:53. DOI:https://doi.org/10.1145/1347375.1347389Google ScholarDigital Library
- Lu Yang, Chaochen Zhou, Naijun Zhan, and Bican Xia. 2010. Recent advances in program verification through computer algebra. Front. Comput. Sci. Chin. 4, 1 (2010), 1--16. DOI:https://doi.org/10.1007/s11704-009-0074-7Google ScholarCross Ref
Index Terms
- Non-polynomial Worst-Case Analysis of Recursive Programs
Recommendations
A MILP approach to DRAM access worst-case analysis
AbstractThe Dynamic Random Access Memory (DRAM) is among the major points of contention in multi-core systems. We consider a challenging optimization problem arising in worst-case performance analysis of systems architectures: computing the ...
Highlights- Exact worst-case delay in COTS DRAM can be computed as a MILP optimum.
- Worst-...
Elementary Yet Precise Worst-Case Analysis of Floyd's Heap-Construction Program
The worst-case behavior of the heap-construction phase of Heapsort escaped mathematically precise characterization by a closed-form formula for almost five decades. This paper offers a proof that the exact number of comparisons of keys performed in the ...
Type-guided worst-case input generation
This paper presents a novel technique for type-guided worst-case input generation for functional programs. The technique builds on automatic amortized resource analysis (AARA), a type-based technique for deriving symbolic bounds on the resource usage of ...
Comments