{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:56Z","timestamp":1775868536735,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":72,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA STAC","award":["FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-15-C-0082"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1801369,1812876,1845514"],"award-info":[{"award-number":["1801369,1812876,1845514"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DARPA AA","award":["FA8750-18-C- 0092"],"award-info":[{"award-number":["FA8750-18-C- 0092"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314602","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"253-268","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Resource-guided program synthesis"],"prefix":"10.1145","author":[{"given":"Tristan","family":"Knoth","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Di","family":"Wang","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_1"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9174-1"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882102"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Arie Gurfinkel Kenneth L. McMillan and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation .  Nikolaj Bj\u00f8rner Arie Gurfinkel Kenneth L. McMillan and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation .","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_2_7_1","volume-title":"Conf. (LPAR\u201910)","author":"Blanc R\u00e9gis","year":"2010","unstructured":"R\u00e9gis Blanc , Thomas A. Henzinger , Thibaud Hottelier , and Laura Kov\u00e1cs . 2010 . ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int . Conf. (LPAR\u201910) . 103\u2013118. R\u00e9gis Blanc, Thomas A. Henzinger, Thibaud Hottelier, and Laura Kov\u00e1cs. 2010. ABC: Algebraic Bound Computation for Loops. In Logic for Prog., AI., and Reasoning - 16th Int. Conf. (LPAR\u201910) . 103\u2013118."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837666"},{"key":"e_1_3_2_2_10_1","volume-title":"Conf. (TACAS\u201914)","author":"Brockschmidt Marc","year":"2014","unstructured":"Marc Brockschmidt , Fabian Emmes , Stephan Falke , Carsten Fuhs , and J\u00fcrgen Giesl . 2014 . Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int . Conf. (TACAS\u201914) . 140\u2013155. Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, and J\u00fcrgen Giesl. 2014. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int. Conf. (TACAS\u201914) . 140\u2013155."},{"key":"e_1_3_2_2_11_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings . 243\u2013259","author":"Cern\u00fd Pavol","year":"2011","unstructured":"Pavol Cern\u00fd , Krishnendu Chatterjee , Thomas A. Henzinger , Arjun Radhakrishna , and Rohit Singh . 2011 . Quantitative Synthesis for Concurrent Programs. In Computer Aided Verification - 23rd International Conference , CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings . 243\u2013259 . Pavol Cern\u00fd, Krishnendu Chatterjee, Thomas A. Henzinger, Arjun Radhakrishna, and Rohit Singh. 2011. Quantitative Synthesis for Concurrent Programs. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings . 243\u2013259."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Pavol Cern\u00fd Edmund M. Clarke Thomas A. Henzinger Arjun Radhakrishna Leonid Ryzhyk Roopsha Samanta and Thorsten Tarrach. 2015. From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. In CAV.  Pavol Cern\u00fd Edmund M. Clarke Thomas A. Henzinger Arjun Radhakrishna Leonid Ryzhyk Roopsha Samanta and Thorsten Tarrach. 2015. From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. In CAV.","DOI":"10.1007\/978-3-319-21668-3_11"},{"key":"e_1_3_2_2_13_1","volume-title":"Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP\u201915)","author":"Cern\u00fd Pavol","year":"2015","unstructured":"Pavol Cern\u00fd , Thomas A. Henzinger , Laura Kov\u00e1cs , Arjun Radhakrishna , and Jakob Zwirchmayr . 2015 . Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP\u201915) . 105\u2013131. Pavol Cern\u00fd, Thomas A. Henzinger, Laura Kov\u00e1cs, Arjun Radhakrishna, and Jakob Zwirchmayr. 2015. Segment Abstraction for Worst-Case Execution Time Analysis. In 24th European Symposium on Programming (ESOP\u201915) . 105\u2013131."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462180"},{"key":"e_1_3_2_2_15_1","volume-title":"Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL\u201917)","author":"Cicek Ezgi","year":"2017","unstructured":"Ezgi Cicek , Gilles Barthe , Marco Gaboardi , Deepak Garg , and Jan Hoffmann . 2017 . Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL\u201917) . Ezgi Cicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL\u201917) ."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_3_2_2_17_1","volume-title":"TACAS (LNCS)","author":"de Moura Leonardo Mendon\u00e7a","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In TACAS (LNCS) , Vol. 4963 . Springer , 337\u2013340. Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337\u2013340."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009851"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192395"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240260"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677008"},{"key":"e_1_3_2_2_29_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper R.","unstructured":"R. Harper . 2016. Practical Foundations for Programming Languages . Cambridge University Press . R. Harper. 2016. Practical Foundations for Programming Languages. Cambridge University Press."},{"key":"e_1_3_2_2_30_1","unstructured":"Jan Hoffmann. 2018. RAML Web Site. http:\/\/raml.co\/ .  Jan Hoffmann. 2018. RAML Web Site. http:\/\/raml.co\/ ."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_2_35_1","volume-title":"TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I . 247\u2013263","author":"Inala Jeevana Priya","year":"2017","unstructured":"Jeevana Priya Inala , Nadia Polikarpova , Xiaokang Qiu , Benjamin S. Lerner , and Armando Solar-Lezama . 2017 . Synthesis of Recursive ADT Transformations from Reusable Templates. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference , TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I . 247\u2013263 . Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, and Armando Solar-Lezama. 2017. Synthesis of Recursive ADT Transformations from Reusable Templates. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I . 247\u2013263."},{"key":"e_1_3_2_2_36_1","volume-title":"Bordeaux","author":"Inala Jeevana Priya","year":"2016","unstructured":"Jeevana Priya Inala , Rohit Singh , and Armando Solar-Lezama . 2016 . Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference , Bordeaux , France, July 5-8, 2016, Proceedings . 302\u2013320. Jeevana Priya Inala, Rohit Singh, and Armando Solar-Lezama. 2016. Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings . 302\u2013320."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542510"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_3_2_2_40_1","volume-title":"Resource-Guided Program Synthesis. CoRR abs\/1904.07415","author":"Knoth Tristan","year":"2019","unstructured":"Tristan Knoth , Di Wang , Nadia Polikarpova , and Jan Hoffmann . 2019. Resource-Guided Program Synthesis. CoRR abs\/1904.07415 ( 2019 ). https:\/\/arxiv.org\/abs\/1904.07415 Tristan Knoth, Di Wang, Nadia Polikarpova, and Jan Hoffmann. 2019. Resource-Guided Program Synthesis. CoRR abs\/1904.07415 (2019). https:\/\/arxiv.org\/abs\/1904.07415"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481848.1481853"},{"key":"e_1_3_2_2_42_1","volume-title":"Integrating Linear and Dependent Types. In Symposium on Principles of Programming Languages (POPL\u201915)","author":"Krishnaswami Neelakantan R.","year":"2015","unstructured":"Neelakantan R. Krishnaswami , Pierre Pradic , and Nick Benton . 2015 . Integrating Linear and Dependent Types. In Symposium on Principles of Programming Languages (POPL\u201915) . Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Symposium on Principles of Programming Languages (POPL\u201915) ."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"crossref","unstructured":"Calvin Loncaric Michael D. Ernst and Emina Torlak. 2018. Generalized Data Structure Synthesis. In ICSE.  Calvin Loncaric Michael D. Ernst and Emina Torlak. 2018. Generalized Data Structure Synthesis. In ICSE.","DOI":"10.1145\/3180155.3180211"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908122"},{"key":"e_1_3_2_2_46_1","volume-title":"Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP\u201917)","author":"Ngo V. C.","unstructured":"V. C. Ngo , Mario Dehesa-Azuara , M. Fredrikson , and J. Hoffmann . 2017 . Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP\u201917) . V. C. Ngo, Mario Dehesa-Azuara, M. Fredrikson, and J. Hoffmann. 2017. Verifying and Synthesizing Constant-Resource Implementations with Types. In Symp. on Sec. and Privacy (SP\u201917)."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_2_2_48_1","unstructured":"Adam Chlipala Peng Wang Di Wang. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In OOPSLA.  Adam Chlipala Peng Wang Di Wang. 2017. TiML: A Functional Language for Practical Complexity Analysis with Invariants. In OOPSLA."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594339"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133889"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_3_2_2_54_1","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI.  Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814278"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364575"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908102"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_3_2_2_65_1","series-title":"SIAM J. Algebraic Discrete Methods 6 (August","volume-title":"Amortized Computational Complexity","author":"Tarjan R. E.","year":"1985","unstructured":"R. E. Tarjan . 1985. Amortized Computational Complexity . SIAM J. Algebraic Discrete Methods 6 (August 1985 ). Issue 2. R. E. Tarjan. 1985. Amortized Computational Complexity. SIAM J. Algebraic Discrete Methods 6 (August 1985). Issue 2."},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_2_2_69_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker D.","unstructured":"D. Walker . 2002. Substructural Type Systems . In Advanced Topics in Types and Programming Languages . MIT Press . D. Walker. 2002. Substructural Type Systems. In Advanced Topics in Types and Programming Languages . MIT Press."},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133887"},{"key":"e_1_3_2_2_73_1","volume-title":"Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symp. (SAS\u201911)","author":"Zuleger Florian","year":"2011","unstructured":"Florian Zuleger , Moritz Sinn , Sumit Gulwani , and Helmut Veith . 2011 . Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symp. (SAS\u201911) . 280\u2013297. Florian Zuleger, Moritz Sinn, Sumit Gulwani, and Helmut Veith. 2011. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symp. (SAS\u201911). 280\u2013297."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314602","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314602","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314602","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314602"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":72,"alternative-id":["10.1145\/3314221.3314602","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314602","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}