{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T04:32:00Z","timestamp":1754109120660,"version":"3.41.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1139021"],"award-info":[{"award-number":["CCF-1139021"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>A key challenge in program synthesis is synthesizing programs that use libraries, which most real-world software does. The current state of the art is to model libraries with mock library implementations that perform the same function in a simpler way. However, mocks may still be large and complex, and must include many implementation details, both of which could limit synthesis performance. To address this problem, we introduce JLibSketch, a Java program synthesis tool that allows library behavior to be described with algebraic specifications, which are rewrite rules for sequences of method calls, e.g., encryption followed by decryption (with the same key) is the identity. JLibSketch implements rewrite rules by compiling JLibSketch problems into problems for the Sketch program synthesis tool. More specifically, after compilation, library calls are represented by abstract data types (ADTs), and rewrite rules manipulate those ADTs. We formalize compilation and prove it sound and complete if the rewrite rules are ordered and non-unifiable. We evaluated JLibSketch by using it to synthesize nine programs that use libraries from three domains: data structures, cryptography, and file systems. We found that algebraic specifications are, on average, about half the size of mocks. We also found that algebraic specifications perform better than mocks on seven of the nine programs, sometimes significantly so, and perform equally well on the last two programs. Thus, we believe that JLibSketch takes an important step toward synthesis of programs that use libraries.<\/jats:p>","DOI":"10.1145\/3360558","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Program synthesis with algebraic library specifications"],"prefix":"10.1145","volume":"3","author":[{"given":"Benjamin","family":"Mariano","sequence":"first","affiliation":[{"name":"University of Maryland at College Park, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josh","family":"Reese","sequence":"additional","affiliation":[{"name":"University of Maryland at College Park, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siyuan","family":"Xu","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ThanhVu","family":"Nguyen","sequence":"additional","affiliation":[{"name":"University of Nebraska-Lincoln, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[{"name":"Tufts University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Solar-Lezama","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"volume-title":"Computing with an SMT Solver","author":"Amin Nada","key":"e_1_2_2_1_1","unstructured":"Nada Amin , K. Rustan M. Leino , and Tiark Rompf . 2014. Computing with an SMT Solver . In Tests and Proofs, Martina Seidl and Nikolai Tillmann (Eds.). Springer International Publishing , Cham , 20\u201335. Nada Amin, K. Rustan M. Leino, and Tiark Rompf. 2014. Computing with an SMT Solver. In Tests and Proofs, Martina Seidl and Nikolai Tillmann (Eds.). Springer International Publishing, Cham, 20\u201335."},{"volume-title":"Term rewriting and all that","author":"Baader Franz","key":"e_1_2_2_2_1","unstructured":"Franz Baader and Tobias Nipkow . 1998. Term rewriting and all that . Cambridge University Press , University Press , Cambridge, UK. Franz Baader and Tobias Nipkow. 1998. Term rewriting and all that. Cambridge University Press, University Press, Cambridge, UK."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062353"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837666"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_20"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2396761.2398507"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_21"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"volume-title":"Handbook of Theoretical Computer Science","author":"Dershowitz Nachum","key":"e_1_2_2_10_1","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud . 1990. Rewrite Systems . In Handbook of Theoretical Computer Science , Volume B: Formal Models and Sematics (B). Elsevier, Cambridge, MA, USA, 243\u2013 320 . Nachum Dershowitz and Jean-Pierre Jouannaud. 1990. Rewrite Systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). Elsevier, Cambridge, MA, USA, 243\u2013320."},{"volume-title":"Rewriting Logic and Its Applications, Peter Csaba \u00d6lveczky (Ed.)","author":"Dur\u00e1n Francisco","key":"e_1_2_2_11_1","unstructured":"Francisco Dur\u00e1n and Jos\u00e9 Meseguer . 2010. A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications . In Rewriting Logic and Its Applications, Peter Csaba \u00d6lveczky (Ed.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 69\u201385. Francisco Dur\u00e1n and Jos\u00e9 Meseguer. 2010. A Church-Rosser Checker Tool for Conditional Order-Sorted Equational Maude Specifications. In Rewriting Logic and Its Applications, Peter Csaba \u00d6lveczky (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 69\u201385."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009851"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294948.1294972"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_19"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70705"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1363102.1363105"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092285"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Inala Jeevana Priya","key":"e_1_2_2_20_1","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 , Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 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, Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 247\u2013263."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/366062.366084"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884856"},{"key":"e_1_2_2_23_1","volume-title":"Foster","author":"Jeon Jinseong","year":"2015","unstructured":"Jinseong Jeon , Xiaokang Qiu , Armando Solar-Lezama , and Jeffrey S . Foster . 2015 a. Adaptive Concretization for Parallel Program Synthesis. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 9207 . Springer International Publishing , Cham, 377\u2013394. Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, and Jeffrey S. Foster. 2015a. Adaptive Concretization for Parallel Program Synthesis. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science), Vol. 9207. Springer International Publishing, Cham, 377\u2013394."},{"key":"e_1_2_2_24_1","volume-title":"Foster","author":"Jeon Jinseong","year":"2015","unstructured":"Jinseong Jeon , Xiaokang Qiu , Armando Solar-Lezama , and Jeffrey S . Foster . 2015 b. JSketch: Sketching for Java. In European Software Engineering Conference and Foundations of Software Engineering (ESEC\/FSE), Tool Demo Track. ACM, Bergamo , Italy, Article 1, 4 pages. Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, and Jeffrey S. Foster. 2015b. JSketch: Sketching for Java. In European Software Engineering Conference and Foundations of Software Engineering (ESEC\/FSE), Tool Demo Track. ACM, Bergamo, Italy, Article 1, 4 pages."},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. B. Bendix. 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebras J. Leech (Ed.). Pergamon Press Oxford 263\u2013297.  D. E. Knuth and P. B. Bendix. 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebras J. Leech (Ed.). Pergamon Press Oxford 263\u2013297.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"volume-title":"Java SE 8 Edition. Pearson Education","author":"Lindholm Tim","key":"e_1_2_2_26_1","unstructured":"Tim Lindholm , Frank Yellin , Gilad Bracha , and Alex Buckley . 2016. The Java Virtual Machine Specification , Java SE 8 Edition. Pearson Education , Redwood City, CA , U.S.A. Tim Lindholm, Frank Yellin, Gilad Bracha, and Alex Buckley. 2016. The Java Virtual Machine Specification, Java SE 8 Edition. Pearson Education, Redwood City, CA , U.S.A."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0236-z"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177730491"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968867"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595767"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630074"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_10"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462195"},{"key":"e_1_2_2_37_1","volume-title":"VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Springer Berlin Heidelberg","author":"Singh Rohit","year":"2014","unstructured":"Rohit Singh , Rishabh Singh , Zhilei Xu , Rebecca Krosnick , and Armando Solar-Lezama . 2014 . Modular Synthesis of Sketches Using Models. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference , VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Springer Berlin Heidelberg , Berlin, Heidelberg, 395\u2013414. Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick, and Armando Solar-Lezama. 2014. Modular Synthesis of Sketches Using Models. In Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19-21, 2014, Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, 395\u2013414."},{"key":"e_1_2_2_38_1","volume-title":"Program Synthesis with Equivalence Reduction. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer","author":"Smith Calvin","year":"2019","unstructured":"Calvin Smith and Aws Albarghouthi . 2019 . Program Synthesis with Equivalence Reduction. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer , Berlin, Heidelberg, 24\u201347. Calvin Smith and Aws Albarghouthi. 2019. Program Synthesis with Equivalence Reduction. In International Conference on Verification, Model Checking, and Abstract Interpretation. Springer, Berlin, Heidelberg, 24\u201347."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_2_40_1","unstructured":"Armando Solar-Lezama. 2016. The Sketch Programmers Manual. MIT. Version 1.7.5.  Armando Solar-Lezama. 2016. The Sketch Programmers Manual. MIT. Version 1.7.5."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250754"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"volume-title":"ASPLOS \u201906","author":"Solar-Lezama Armando","key":"e_1_2_2_43_1","unstructured":"Armando Solar-Lezama , Liviu Tancau , Rastislav Bodik , Vijay Saraswat , and Sanjit Seshia . 2006. Combinatorial Sketching for Finite Programs . In ASPLOS \u201906 . ACM Press , San Jose, CA, USA , Article 1, 12 pages. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, and Sanjit Seshia. 2006. Combinatorial Sketching for Finite Programs. In ASPLOS \u201906. ACM Press, San Jose, CA, USA, Article 1, 12 pages."},{"key":"e_1_2_2_44_1","volume-title":"SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. Springer Berlin Heidelberg","author":"Suter Philippe","year":"2011","unstructured":"Philippe Suter , Ali Sinan K\u00f6ksal , and Viktor Kuncak . 2011 . Satisfiability Modulo Recursive Programs. In Static Analysis -18th International Symposium , SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. Springer Berlin Heidelberg , Berlin, Heidelberg, 298\u2013315. Philippe Suter, Ali Sinan K\u00f6ksal, and Viktor Kuncak. 2011. Satisfiability Modulo Recursive Programs. In Static Analysis -18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, 298\u2013315."},{"volume-title":"PLDI\u201914","author":"Torlak Emina","key":"e_1_2_2_45_1","unstructured":"Emina Torlak and Rastislav Bodik . 2014. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages . In PLDI\u201914 . ACM , Edinburgh, UK , 530\u2013541. Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages. In PLDI\u201914. ACM, Edinburgh, UK, 530\u2013541."},{"key":"e_1_2_2_46_1","volume-title":"Article 1 (Feb.","author":"van der Merwe Heila","year":"2015","unstructured":"Heila van der Merwe , Oksana Tkachuk , Brink van der Merwe , and Willem Visser . 2015. Generation of Library Models for Verification of Android Applications. SIGSOFT Softw. Eng. Notes 40, 1 , Article 1 (Feb. 2015 ), 5 pages. Heila van der Merwe, Oksana Tkachuk, Brink van der Merwe, and Willem Visser. 2015. Generation of Library Models for Verification of Android Applications. SIGSOFT Softw. Eng. Notes 40, 1, Article 1 (Feb. 2015), 5 pages."},{"key":"e_1_2_2_47_1","volume-title":"POPL","author":"Vazou Niki","year":"2018","unstructured":"Niki Vazou , Anish Tondwalkar , Vikraman Choudhury , Ryan G. Scott , Ryan R. Newton , Philip Wadler , and Ranjit Jhala . 2018. Refinement reflection: complete verification with SMT. PACMPL 2 , POPL ( 2018 ), 53:1\u201353:31. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. 2018. Refinement reflection: complete verification with SMT. PACMPL 2, POPL (2018), 53:1\u201353:31."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133886"},{"key":"e_1_2_2_49_1","unstructured":"David Wheeler. 2009. SLOCcount. http:\/\/www.dwheeler.com\/sloccount\/  David Wheeler. 2009. SLOCcount. http:\/\/www.dwheeler.com\/sloccount\/"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360558","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360558","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360558","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360558"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":49,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360558"],"URL":"https:\/\/doi.org\/10.1145\/3360558","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}