{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:26:11Z","timestamp":1745994371800,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Determining upper bounds on the time complexity of a program is a fundamental problem with a variety of applications, such as performance debugging, resource certification, and compile-time optimizations. Automated techniques for cost analysis excel at bounding the resource complexity of programs that use integer values and linear arithmetic. Unfortunately, they fall short when execution traces become more involved, esp. when data dependencies may affect the termination conditions of loops. In such cases, state-of-the-art analyzers have shown to produce loose bounds, or even no bound at all.<\/jats:p><jats:p>We propose a novel technique that generalizes the common notion of recurrence relations based on ranking functions. Existing methods usually unfold one loop iteration, and examine the resulting relations between variables. These relations assist in establishing a recurrence that bounds the number of loop iterations. We propose a different approach, where we derive recurrences by comparing<jats:italic>whole traces<\/jats:italic>with<jats:italic>whole traces<\/jats:italic>of a lower rank, avoiding the need to analyze the complexity of intermediate states. We offer a set of global properties, defined with respect to whole traces, that facilitate such a comparison, and show that these properties can be checked efficiently using a handful of local conditions. To this end, we adapt<jats:italic>state squeezers<\/jats:italic>, an induction mechanism previously used for verifying safety properties. We demonstrate that this technique encompasses the reasoning power of bounded unfolding, and more. We present some seemingly innocuous, yet intricate, examples where previous tools based on<jats:italic>cost relations<\/jats:italic>and control flow analysis fail to solve, and that our squeezer-powered approach succeeds.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_12","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"320-347","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Run-time Complexity Bounds Using Squeezers"],"prefix":"10.1007","author":[{"given":"Oren","family":"Ish-Shalom","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"12_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 313\u2013321. IEEE Computer Society (1996)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109\u2013127 (2000)","DOI":"10.1006\/inco.1999.2843"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Automatic inference of upper bounds for recurrence relations in cost analysis. In: Alpuente, M., Vidal, G. (eds.) Static Analysis. pp. 221\u2013237. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-69166-2_15"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for java bytecode. In: Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures. pp. 113\u2013132 (2007)","DOI":"10.1007\/978-3-540-92188-2_5"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Albert, E., Bofill, M., Borralleras, C., Martin-Martin, E., Rubio, A.: Resource analysis driven by (conditional) termination proofs. Theory Pract. Log. Program. 19(5-6), 722\u2013739 (2019). https:\/\/doi.org\/10.1017\/S1471068419000152, https:\/\/doi.org\/10.1017\/S1471068419000152","DOI":"10.1017\/S1471068419000152"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Min\u00e9, A., Schmidt, D. (eds.) Static Analysis. pp. 405\u2013421. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-33125-1_27"},{"key":"12_CR7","unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol.\u00a040, pp. 1\u201325. IOS Press (2015)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. 30(3) (May 2008)","DOI":"10.1145\/1353445.1353450"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Breck, J., Cyphert, J., Kincaid, Z., Reps, T.: Templates and recurrences: Better together. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 688\u2013702. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020)","DOI":"10.1145\/3385412.3386035"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08413, pp. 140\u2013155. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"12_CR11","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. pp. 209\u2013224. OSDI\u201908, USENIX Association, Berkeley, CA, USA (2008), http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855756"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. p. 84\u201396. POPL \u201978, Association for Computing Machinery, New York, NY, USA (1978)","DOI":"10.1145\/512760.512770"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. TACAS\u201908\/ETAPS\u201908, Springer-Verlag, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Debray, S.K., Lin, N.W.: Cost analysis of logic programs. ACM Trans. Program. Lang. Syst. 15(5), 826\u2013875 (Nov 1993)","DOI":"10.1145\/161468.161472"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! THEORETICAL COMPUTER SCIENCE 256(1), 2001 (1998)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. vol.\u00a09995, pp. 254\u2013273 (11 2016)","DOI":"10.1007\/978-3-319-48989-6_16"},{"key":"12_CR17","unstructured":"Gulwani, S.: The reachability-bound problem. Tech. Rep. MSR-TR-2009-146 (October 2009), https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-reachability-bound-problem\/"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 375\u2013385. PLDI \u201909, Association for Computing Machinery, New York, NY, USA (2009)","DOI":"10.1145\/1542476.1542518"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: Shao, Z., Pierce, B.C. (eds.) POPL. pp. 127\u2013139. ACM (2009), http:\/\/dblp.uni-trier.de\/db\/conf\/popl\/popl2009.html#GulwaniMC09","DOI":"10.1145\/1480881.1480898"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ML. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol.\u00a07358, pp. 781\u2013786. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential: A static inference of polynomial bounds for functional programs (extended version) (03 2010)","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: Beyer, D., Zufferey, D. (eds.) Verification, Model Checking, and Abstract Interpretation - 21st International Conference, VMCAI 2020, New Orleans, LA, USA, January 16-21, 2020, Proceedings. Lecture Notes in Computer Science, vol. 11990, pp. 112\u2013135. Springer (2020)","DOI":"10.1007\/978-3-030-39322-9_6"},{"key":"12_CR23","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. CoRR abs\/1405.4028 (2014), http:\/\/arxiv.org\/abs\/1405.4028"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 81\u201392. POPL \u201901, Association for Computing Machinery, New York, NY, USA (2001)","DOI":"10.1145\/360204.360210"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification. pp. 401\u2013414. Springer Berlin Heidelberg, Berlin, Heidelberg (2006)","DOI":"10.1007\/11817963_36"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Mera, E., L\u00f3pez-Garc\u00eda, P., Puebla, G., Carro, M., Hermenegildo, M.V.: Combining static analysis and profiling for estimating execution times. In: International Symposium on Practical Aspects of Declarative Languages. pp. 140\u2013154. Springer (2007)","DOI":"10.1007\/978-3-540-69611-7_9"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reasoning 59(1), 3\u201345 (2017)","DOI":"10.1007\/s10817-016-9402-4"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528\u2013539 (Sep 1975)","DOI":"10.1145\/361002.361016"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) Static Analysis. pp. 280\u2013297. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:45:57Z","timestamp":1671684357000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}