{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:54:32Z","timestamp":1721894072228},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006602","name":"AFRL","doi-asserted-by":"crossref","award":["8750-14-2-0270"],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1453386"],"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":[[2017,10,12]]},"abstract":"\n In application domains that store data in a tabular format, a common task is to fill the values of some cells using values stored in other cells. For instance, such data completion tasks arise in the context of\n missing value imputation<\/jats:italic>\n in data science and\n derived data<\/jats:italic>\n computation in spreadsheets and relational databases. Unfortunately, end-users and data scientists typically struggle with many data completion tasks that require non-trivial programming expertise. This paper presents a synthesis technique for automating data completion tasks using\n programming-by-example (PBE)<\/jats:italic>\n and a very lightweight sketching approach. Given a\n formula sketch<\/jats:italic>\n (e.g., AVG(?\n 1<\/jats:sub>\n , ?\n 2<\/jats:sub>\n )) and a few input-output examples for each hole, our technique synthesizes a program to automate the desired data completion task. Towards this goal, we propose a domain-specific language (DSL) that combines spatial and relational reasoning over tabular data and a novel synthesis algorithm that can generate DSL programs that are consistent with the input-output examples. The key technical novelty of our approach is a new version space learning algorithm that is based on\n finite tree automata<\/jats:italic>\n (FTA). The use of FTAs in the learning algorithm leads to a more compact representation that allows more sharing between programs that are consistent with the examples. We have implemented the proposed approach in a tool called DACE and evaluate it on 84 benchmarks taken from online help forums. We also illustrate the advantages of our approach by comparing our technique against two existing synthesizers, namely Prose and Sketch.\n <\/jats:p>","DOI":"10.1145\/3133886","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T15:15:45Z","timestamp":1507907745000},"page":"1-26","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Synthesis of data completion scripts using finite tree automata"],"prefix":"10.1145","volume":"1","author":[{"given":"Xinyu","family":"Wang","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Rishabh","family":"Singh","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70844-5_22"},{"key":"e_1_2_1_2_1","volume-title":"Recursive Program Synthesis (CAV)","author":"Albarghouthi Aws","unstructured":"Aws Albarghouthi , Sumit Gulwani , and Zachary Kincaid . 2013. Recursive Program Synthesis (CAV) . Springer-Verlag , 934\u2013950. Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis (CAV). Springer-Verlag, 934\u2013950."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_10"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"James Bornholt Emina Torlak Dan Grossman and Luis Ceze. 2016. Optimizing Synthesis with Metasketches (POPL). ACM 775\u2013788. James Bornholt Emina Torlak Dan Grossman and Luis Ceze. 2016. Optimizing Synthesis with Metasketches (POPL). ACM 775\u2013788.","DOI":"10.1145\/2914770.2837666"},{"key":"e_1_2_1_5_1","volume-title":"Deterministic Automata on Unranked Trees (FCT)","author":"Cristau Julien","unstructured":"Julien Cristau , Christof L\u00f6ding , and Wolfgang Thomas . 2005. Deterministic Automata on Unranked Trees (FCT) . SpringerVerlag , 68\u201379. Julien Cristau, Christof L\u00f6ding, and Wolfgang Thomas. 2005. Deterministic Automata on Unranked Trees (FCT). SpringerVerlag, 68\u201379."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"John K. Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-output Examples (PLDI). ACM 229\u2013239. John K. Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-output Examples (PLDI). ACM 229\u2013239.","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-output Examples (POPL). ACM 317\u2013330. Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-output Examples (POPL). ACM 317\u2013330.","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/767193.767195"},{"key":"e_1_2_1_10_1","volume-title":"Gallagher","author":"Kafle Bishoksan","year":"2015","unstructured":"Bishoksan Kafle and John P . Gallagher . 2015 . Tree Automata-Based Refinement with Application to Horn Clause Verification (VMCAI 2015) . Springer-Verlag New York , Inc., 209\u2013226. Bishoksan Kafle and John P. Gallagher. 2015. Tree Automata-Based Refinement with Application to Horn Clause Verification (VMCAI 2015) . Springer-Verlag New York, Inc., 209\u2013226."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01492-5_14"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025671410623"},{"key":"e_1_2_1_14_1","unstructured":"Parthasarathy Madhusudan. 2011. Synthesizing Reactive Programs. In Computer Science Logic. 428\u2013442. Parthasarathy Madhusudan. 2011. Synthesizing Reactive Programs. In Computer Science Logic. 428\u2013442."},{"key":"e_1_2_1_15_1","volume-title":"Minimizing Tree Automata for Unranked Trees","author":"Martens Wim","unstructured":"Wim Martens and Joachim Niehren . 2005. Minimizing Tree Automata for Unranked Trees . Springer Berlin Heidelberg , 232\u2013246. Wim Martens and Joachim Niehren. 2005. Minimizing Tree Automata for Unranked Trees. Springer Berlin Heidelberg, 232\u2013246."},{"key":"e_1_2_1_16_1","unstructured":"Jonathan May and Kevin Knight. 2008. A Primer on Tree Automata Software for Natural Language Processing. (2008). Jonathan May and Kevin Knight. 2008. A Primer on Tree Automata Software for Natural Language Processing. (2008)."},{"key":"e_1_2_1_17_1","volume-title":"Generalization as search. Artificial intelligence 18, 2","author":"Mitchell Tom M","year":"1982","unstructured":"Tom M Mitchell . 1982. Generalization as search. Artificial intelligence 18, 2 ( 1982 ), 203\u2013226. Tom M Mitchell. 1982. Generalization as search. Artificial intelligence 18, 2 (1982), 203\u2013226."},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed Program Synthesis (PLDI). ACM 619\u2013630. Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed Program Synthesis (PLDI). ACM 619\u2013630.","DOI":"10.1145\/2813885.2738007"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 13th IASTED International Conference on Robotics and Applications (RA) . ACTA Press, 394\u2013399","author":"Pardowitz Michael","year":"2007","unstructured":"Michael Pardowitz , Bernhard Glaser , and R\u00fcdiger Dillmann . 2007 . Learning Repetitive Robot Programs from Demonstrations Using Version Space Algebra . In Proceedings of the 13th IASTED International Conference on Robotics and Applications (RA) . ACTA Press, 394\u2013399 . Michael Pardowitz, Bernhard Glaser, and R\u00fcdiger Dillmann. 2007. Learning Repetitive Robot Programs from Demonstrations Using Version Space Algebra. In Proceedings of the 13th IASTED International Conference on Robotics and Applications (RA) . ACTA Press, 394\u2013399."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types (PLDI) . ACM 522\u2013538. Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types (PLDI) . ACM 522\u2013538.","DOI":"10.1145\/2980983.2908093"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A Framework for Inductive Program Synthesis (OOPSLA). ACM 107\u2013126. Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A Framework for Inductive Program Synthesis (OOPSLA). ACM 107\u2013126.","DOI":"10.1145\/2858965.2814310"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Eric Schkufza Rahul Sharma and Alex Aiken. 2013. Stochastic Superoptimization (ASPLOS). 305\u2013316. Eric Schkufza Rahul Sharma and Alex Aiken. 2013. Stochastic Superoptimization (ASPLOS). 305\u2013316.","DOI":"10.1145\/2499368.2451150"},{"key":"e_1_2_1_23_1","volume-title":"Synthesizing number transformations from input-output examples (CAV)","author":"Singh Rishabh","unstructured":"Rishabh Singh and Sumit Gulwani . 2012. Synthesizing number transformations from input-output examples (CAV) . Springer , 634\u2013651. Rishabh Singh and Sumit Gulwani. 2012. Synthesizing number transformations from input-output examples (CAV). Springer, 634\u2013651."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis (PLDI). ACM 326\u2013340. Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis (PLDI). ACM 326\u2013340.","DOI":"10.1145\/2980983.2908102"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Gilad Arnold Liviu Tancau Rastislav Bodik Vijay Saraswat and Sanjit Seshia. 2007. Sketching Stencils (PLDI). ACM 167\u2013178. Armando Solar-Lezama Gilad Arnold Liviu Tancau Rastislav Bodik Vijay Saraswat and Sanjit Seshia. 2007. Sketching Stencils (PLDI). ACM 167\u2013178.","DOI":"10.1145\/1273442.1250754"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Rodric Rabbah Rastislav Bod\u00edk and Kemal Ebcio\u011flu. 2005. Programming by Sketching for Bit-streaming Programs (PLDI). ACM 281\u2013294. Armando Solar-Lezama Rodric Rabbah Rastislav Bod\u00edk and Kemal Ebcio\u011flu. 2005. Programming by Sketching for Bit-streaming Programs (PLDI). ACM 281\u2013294.","DOI":"10.1145\/1064978.1065045"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs (ASPLOS). ACM 404\u2013415. Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs (ASPLOS). ACM 404\u2013415.","DOI":"10.1145\/1168918.1168907"},{"key":"e_1_2_1_28_1","first-page":"57","article-title":"Generalized finite automata theory with an application to a decision problem of second-order logic","volume":"2","author":"Thatcher James W","year":"1968","unstructured":"James W Thatcher and Jesse B Wright . 1968 . Generalized finite automata theory with an application to a decision problem of second-order logic . Theory of Computing Systems 2 , 1 (1968), 57 \u2013 81 . James W Thatcher and Jesse B Wright. 1968. Generalized finite automata theory with an application to a decision problem of second-order logic. Theory of Computing Systems 2, 1 (1968), 57\u201381.","journal-title":"Theory of Computing Systems"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Abhishek Udupa Arun Raghavan Jyotirmoy V. Deshmukh Sela Mador-Haim Milo M. K. Martin and Rajeev Alur. 2013. TRANSIT: specifying protocols with concolic snippets (PLDI). 287\u2013296. Abhishek Udupa Arun Raghavan Jyotirmoy V. Deshmukh Sela Mador-Haim Milo M. K. Martin and Rajeev Alur. 2013. TRANSIT: specifying protocols with concolic snippets (PLDI). 287\u2013296.","DOI":"10.1145\/2499370.2462174"},{"key":"e_1_2_1_30_1","volume-title":"FIDEX: Filtering Spreadsheet Data using Examples (OOPSLA). ACM, 195\u2013213.","author":"Wang Xinyu","year":"2016","unstructured":"Xinyu Wang , Sumit Gulwani , and Rishabh Singh . 2016 . FIDEX: Filtering Spreadsheet Data using Examples (OOPSLA). ACM, 195\u2013213. Xinyu Wang, Sumit Gulwani, and Rishabh Singh. 2016. FIDEX: Filtering Spreadsheet Data using Examples (OOPSLA). ACM, 195\u2013213."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Navid Yaghmazadeh Christian Klinger Isil Dillig and Swarat Chaudhuri. 2016. Synthesizing Transformations on Hierarchically Structured Data (PLDI). ACM 508\u2013521. Navid Yaghmazadeh Christian Klinger Isil Dillig and Swarat Chaudhuri. 2016. Synthesizing Transformations on Hierarchically Structured Data (PLDI). ACM 508\u2013521.","DOI":"10.1145\/2980983.2908088"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133886","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T21:15:34Z","timestamp":1672521334000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133886"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":30,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133886"],"URL":"https:\/\/doi.org\/10.1145\/3133886","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}