{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:15Z","timestamp":1751662875297,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"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,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"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>We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a<jats:italic>concrete<\/jats:italic>expression exactly describing resource usage, whereas our method uses big-<jats:italic>O<\/jats:italic>notation to specify the<jats:italic>asymptotic<\/jats:italic>resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity<jats:inline-formula><jats:alternatives><jats:tex-math>$$O(n\\log (n))$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>O<\/mml:mi><mml:mo>(<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>log<\/mml:mo><mml:mo>(<\/mml:mo><mml:mi>n<\/mml:mi><mml:mo>)<\/mml:mo><mml:mo>)<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p><jats:p>Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These typing rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool,<jats:sc>SynPlexity<\/jats:sc>, was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_37","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"783-807","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Synthesis with Asymptotic Resource Bounds"],"prefix":"10.1007","author":[{"given":"Qinheping","family":"Hu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Cyphert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Loris","family":"D\u2019Antoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"37_CR1","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1023\/A:1018373005182","volume":"10","author":"M Akra","year":"1998","unstructured":"Akra, M., Bazzi, L.: On the solution of linear recurrence equations. Comput. Optim. Appl. 10, 195\u2013210 (1998)","journal-title":"Comput. Optim. Appl."},{"key":"37_CR2","doi-asserted-by":"publisher","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, Germ\u00e1n, P.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46, 161\u2013203 (2011) https:\/\/doi.org\/10.1007\/s10817-010-9174-1","DOI":"10.1007\/s10817-010-9174-1"},{"issue":"3","key":"37_CR3","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1008861.1008865","volume":"12","author":"JL Bentley","year":"1980","unstructured":"Bentley, J.L., Haken, D., Saxe, J.B.: A general method for solving divide-and-conquer recurrences. ACM SIGACT News 12(3), 36\u201344 (1980)","journal-title":"ACM SIGACT News"},{"key":"37_CR4","doi-asserted-by":"crossref","unstructured":"Breck, J., Cyphert, J., Kincaid, Z., Reps, T.: Templates and recurrences: better together. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI (2020)","DOI":"10.1145\/3395656"},{"key":"37_CR5","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3nd edn. The MIT Press, Cambridge (2009)"},{"issue":"4","key":"37_CR6","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-016-9378-0","volume":"58","author":"M Eberl","year":"2016","unstructured":"Eberl, M.: Proving divide and conquer complexities in Isabelle\/HOL. J. Autom. Reasoning 58(4), 483\u2013508 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9378-0","journal-title":"J. Autom. Reasoning"},{"key":"37_CR7","unstructured":"Flores Montoya, A.: Cost Analysis of Programs Based on the Refinement of Cost Relations. Ph.D. thesis, TU Darmstadt (2017)"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-319-89884-1_19","volume-title":"Programming Languages and Systems","author":"A Gu\u00e9neau","year":"2018","unstructured":"Gu\u00e9neau, A., Chargu\u00e9raud, A., Pottier, F.: A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 533\u2013560. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_19"},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 357\u2013370 (2011)","DOI":"10.1145\/1925844.1926427"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Resource aware ml. In: The International Conference on Computer Aided Verification, CAV (2012)","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"37_CR11","doi-asserted-by":"crossref","unstructured":"Hu, Q., Cyphert, J., D\u2019Antoni, L., Reps, T.: Synthesis with asymptotic resource bounds. arXiv preprint arXiv:2103.04188 (2021)","DOI":"10.1007\/978-3-030-81685-8_37"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-319-96145-3_21","volume-title":"Computer Aided Verification","author":"Q Hu","year":"2018","unstructured":"Hu, Q., D\u2019Antoni, L.: Syntax-guided synthesis with quantitative syntactic objectives. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 386\u2013403. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_21"},{"key":"37_CR13","doi-asserted-by":"publisher","unstructured":"Kauers, M., Paule, P.: The Concrete Tetrahedron: Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Springer, Cham (2011) https:\/\/doi.org\/10.1007\/978-3-7091-0445-3","DOI":"10.1007\/978-3-7091-0445-3"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Khan, D.M., Hoffmann, J.: Exponential automatic amortized resource analysis. In: International Conference on Foundations of Software Science and Computation Structures. FoSSaCs (2020)","DOI":"10.1007\/978-3-030-45231-5_19"},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.: Non-linear reasoning for invariant synthesis. In: ACM SIGPLAN Symposium on Principles of Programming Languages, POPL (2018)","DOI":"10.1145\/3158142"},{"key":"37_CR16","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.: Resource-guided program synthesis. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 253\u2013268 (2019)","DOI":"10.1145\/3314221.3314602"},{"issue":"1","key":"37_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/345099.345100","volume":"22","author":"BC Pierce","year":"2000","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. (TOPLAS) 22(1), 1\u201344 (2000)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"6","key":"37_CR18","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1145\/2980983.2908093","volume":"51","author":"N Polikarpova","year":"2016","unstructured":"Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. ACM SIGPLAN Notices 51(6), 522\u2013538 (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"Wang, P., Wang, D., Chlipala, A.: Timl: A functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA), 1\u201326 (2017)","DOI":"10.1145\/3133903"},{"key":"37_CR20","doi-asserted-by":"crossref","unstructured":"Wegbreit, B.: Mechanical program analysis. In: Communications of the ACM (1975)","DOI":"10.1145\/361002.361016"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,4]],"date-time":"2023-01-04T18:42:47Z","timestamp":1672857767000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_37","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":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"290","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":"63","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":"22% - 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","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":"12","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":"16 tool papers and 5 invited papers are also included.","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)"}}]}}