{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T04:53:50Z","timestamp":1754110430365,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"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":["1846327"],"award-info":[{"award-number":["1846327"]}],"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":[[2020,1]]},"abstract":"<jats:p>Example-based specifications for program synthesis are inherently ambiguous and may cause synthesizers to generate programs that do not exhibit intended behavior on unseen inputs. Existing synthesis techniques attempt to address this problem by either placing a domain-specific syntactic bias on the hypothesis space or heavily relying on user feedback to help resolve ambiguity.<\/jats:p>\n          <jats:p>We present a new framework to address the ambiguity\/generalizability problem in example-based synthesis. The key feature of our framework is that it places a semantic bias on the hypothesis space using \"relational perturbation properties\" that relate the perturbation\/change in a program output to the perturbation\/change in a program input. An example of such a property is permutation invariance: the program output does not change when the elements of the program input (array) are permuted. The framework is portable across multiple domains and synthesizers and is based on two core steps: (1) automatically augment the set of user-provided examples by \"applying\" relational perturbation properties and (2) use a generic example-based synthesizer to generate a program consistent with the augmented set of examples. Our framework can be instantiated with three different user interfaces, with varying degrees of user engagement to help infer relevant relational perturbation properties. This includes an interface in which the user only provides examples and our framework automatically infers relevant properties. We implement our framework in a tool SKETCHAX specialized to the SKETCH synthesizer and demonstrate that SKETCHAX is effective in significantly boosting the performance of SKETCH for all three user interfaces.<\/jats:p>","DOI":"10.1145\/3371124","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Augmented example-based synthesis using relational perturbation properties"],"prefix":"10.1145","volume":"4","author":[{"given":"Shengwei","family":"An","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rishabh","family":"Singh","sequence":"additional","affiliation":[{"name":"Google, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roopsha","family":"Samanta","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2019. Syntax-Guided Synthesis Competition. https:\/\/sygus.org\/ .  2019. Syntax-Guided Synthesis Competition. https:\/\/sygus.org\/ ."},{"key":"e_1_2_2_2_1","unstructured":"2019. Sketch Benchmarks Repositories. https:\/\/bitbucket.org\/gatoatigrado\/sketch-frontend\/src .  2019. Sketch Benchmarks Repositories. https:\/\/bitbucket.org\/gatoatigrado\/sketch-frontend\/src ."},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Rastislav Bod\u00edk Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In Formal Methods in Computer-Aided Design (FMCAD) . 1\u20138.  Rajeev Alur Rastislav Bod\u00edk Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In Formal Methods in Computer-Aided Design (FMCAD) . 1\u20138.","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_4_1","volume-title":"International Conference on Learning Representations (ICLR).","author":"Balog Matej","year":"2017","unstructured":"Matej Balog , Alexander L. Gaunt , Marc Brockschmidt , Sebastian Nowozin , and Daniel Tarlow . 2017 . DeepCoder: Learning to Write Programs . In International Conference on Learning Representations (ICLR). Matej Balog, Alexander L. Gaunt, Marc Brockschmidt, Sebastian Nowozin, and Daniel Tarlow. 2017. DeepCoder: Learning to Write Programs. In International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_5_1","article-title":"Metamorphic Testing","volume":"51","author":"Chen Tsong Yueh","year":"2018","unstructured":"Tsong Yueh Chen , Fei-Ching Kuo , Huai Liu , Pak-Lok Poon , Dave Towey , T. H. Tse , and Zhi Quan Zhou . 2018 . Metamorphic Testing : A Review of Challenges and Opportunities. Comput. Surveys 51 , 1 (2018), 4:1\u20134:27. Tsong Yueh Chen, Fei-Ching Kuo, Huai Liu, Pak-Lok Poon, Dave Towey, T. H. Tse, and Zhi Quan Zhou. 2018. Metamorphic Testing: A Review of Challenges and Opportunities. Comput. Surveys 51, 1 (2018), 4:1\u20134:27.","journal-title":"A Review of Challenges and Opportunities. Comput. Surveys"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Alessandro Cimatti Anders Franz\u00e9n Alberto Griggio Roberto Sebastiani and Cristian Stenico. 2010. Satisfiability Modulo the Theory of Costs: Foundations and Applications. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . 99\u2013113.  Alessandro Cimatti Anders Franz\u00e9n Alberto Griggio Roberto Sebastiani and Cristian Stenico. 2010. Satisfiability Modulo the Theory of Costs: Foundations and Applications. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . 99\u2013113.","DOI":"10.1007\/978-3-642-12002-2_8"},{"key":"e_1_2_2_7_1","volume-title":"International Conference on Machine Learning (ICML). 990\u2013998","author":"Devlin Jacob","year":"2017","unstructured":"Jacob Devlin , Jonathan Uesato , Surya Bhupatiraju , Rishabh Singh , Abdel-rahman Mohamed, and Pushmeet Kohli . 2017 . RobustFill: Neural Program Learning under Noisy I\/O . In International Conference on Machine Learning (ICML). 990\u2013998 . Jacob Devlin, Jonathan Uesato, Surya Bhupatiraju, Rishabh Singh, Abdel-rahman Mohamed, and Pushmeet Kohli. 2017. RobustFill: Neural Program Learning under Noisy I\/O. In International Conference on Machine Learning (ICML). 990\u2013998."},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Dana Drachsler-Cohen Sharon Shoham and Eran Yahav. 2017. Synthesis with Abstract Examples. In Computer Aided Verification (CAV) . 254\u2013278.  Dana Drachsler-Cohen Sharon Shoham and Eran Yahav. 2017. Synthesis with Abstract Examples. In Computer Aided Verification (CAV) . 254\u2013278.","DOI":"10.1007\/978-3-319-63387-9_13"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"John K. Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In Programming Language Design and Implementation (PLDI). 229\u2013239.  John K. Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In Programming Language Design and Implementation (PLDI). 229\u2013239.","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2011. Automating String Processing in Spreadsheets using Input-Output Examples. In Principles of Programming Languages (POPL) . 317\u2013330.  Sumit Gulwani. 2011. Automating String Processing in Spreadsheets using Input-Output Examples. In Principles of Programming Languages (POPL) . 317\u2013330.","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_2"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240260"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158090"},{"key":"e_1_2_2_15_1","volume-title":"Oracle-guided Component-based Program Synthesis. In International Conference on Software Engineering (ICSE). 215\u2013224","author":"Jha Susmit","year":"2010","unstructured":"Susmit Jha , Sumit Gulwani , Sanjit A. Seshia , and Ashish Tiwari . 2010 . Oracle-guided Component-based Program Synthesis. In International Conference on Software Engineering (ICSE). 215\u2013224 . Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. 2010. Oracle-guided Component-based Program Synthesis. In International Conference on Software Engineering (ICSE). 215\u2013224."},{"key":"e_1_2_2_16_1","volume-title":"Verification &amp","author":"Kanewala Upulee","year":"2016","unstructured":"Upulee Kanewala , James M Bieman , and Asa Ben-Hur . 2016. Predicting Metamorphic Relations for Testing Scientific Software: A Machine Learning Approach using Graph Kernels. Software Testing , Verification &amp ; Reliability 26, 3 ( 2016 ), 245\u2013269. Upulee Kanewala, James M Bieman, and Asa Ben-Hur. 2016. Predicting Metamorphic Relations for Testing Scientific Software: A Machine Learning Approach using Graph Kernels. Software Testing, Verification &amp; Reliability 26, 3 (2016), 245\u2013269."},{"key":"e_1_2_2_17_1","first-page":"1097","article-title":"ImageNet Classification with Deep Convolutional Neural Networks","volume":"25","author":"Krizhevsky Alex","year":"2012","unstructured":"Alex Krizhevsky , Ilya Sutskever , and Geoffrey E. Hinton . 2012 . ImageNet Classification with Deep Convolutional Neural Networks . In Advances in Neural Information Processing Systems (NIPS) 25. 1097 \u2013 1105 . Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton. 2012. ImageNet Classification with Deep Convolutional Neural Networks. In Advances in Neural Information Processing Systems (NIPS) 25. 1097\u20131105.","journal-title":"Advances in Neural Information Processing Systems (NIPS)"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Alan Leung John Sarracino and Sorin Lerner. 2015. Interactive Parser Synthesis by Example. In Programming Language Design and Implementation (PLDI) . 565\u2013574.  Alan Leung John Sarracino and Sorin Lerner. 2015. Interactive Parser Synthesis by Example. In Programming Language Design and Implementation (PLDI) . 565\u2013574.","DOI":"10.1145\/2813885.2738002"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/330534.330543"},{"key":"e_1_2_2_20_1","unstructured":"Henry Lieberman. 2001. Your Wish is My Command: Programming by Example. Morgan Kaufmann.  Henry Lieberman. 2001. Your Wish is My Command: Programming by Example. Morgan Kaufmann."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807442.2807459"},{"key":"e_1_2_2_22_1","volume-title":"NeuroSymbolic Program Synthesis. In International Conference on Learning Representations (ICLR).","author":"Parisotto Emilio","year":"2017","unstructured":"Emilio Parisotto , Abdel-rahman Mohamed, Rishabh Singh , Lihong Li , Dengyong Zhou , and Pushmeet Kohli . 2017 . NeuroSymbolic Program Synthesis. In International Conference on Learning Representations (ICLR). Emilio Parisotto, Abdel-rahman Mohamed, Rishabh Singh, Lihong Li, Dengyong Zhou, and Pushmeet Kohli. 2017. NeuroSymbolic Program Synthesis. In International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180189"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Veselin Raychev Pavol Bielik Martin Vechev and Andreas Krause. 2016. Learning Programs from Noisy Data. In Principles of Programming Languages (POPL) . 761\u2013774.  Veselin Raychev Pavol Bielik Martin Vechev and Andreas Krause. 2016. Learning Programs from Noisy Data. In Principles of Programming Languages (POPL) . 761\u2013774.","DOI":"10.1145\/2914770.2837671"},{"volume-title":"International Conference on Document Analysis and Recognition (ICDAR). 958\u2013962","author":"Simard Patrice Y.","key":"e_1_2_2_25_1","unstructured":"Patrice Y. Simard , David Steinkraus , and John C. Platt . 2003. Best Practices for Convolutional Neural Networks Applied to Visual Document Analysis . In International Conference on Document Analysis and Recognition (ICDAR). 958\u2013962 . Patrice Y. Simard, David Steinkraus, and John C. Platt. 2003. Best Practices for Convolutional Neural Networks Applied to Visual Document Analysis. In International Conference on Document Analysis and Recognition (ICDAR). 958\u2013962."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.14778\/2977797.2977807"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Rishabh Singh and Sumit Gulwani. 2012. Synthesizing Number Transformations from Input-Output Examples. In Computer Aided Verification (CAV) . 634\u2013651.  Rishabh Singh and Sumit Gulwani. 2012. Synthesizing Number Transformations from Input-Output Examples. In Computer Aided Verification (CAV) . 634\u2013651.","DOI":"10.1007\/978-3-642-31424-7_44"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Rishabh Singh and Sumit Gulwani. 2015. Predicting a Correct Program in Programming by Example. In Computer Aided Verificationi (CAV) . 398\u2013414.  Rishabh Singh and Sumit Gulwani. 2015. Predicting a Correct Program in Programming by Example. In Computer Aided Verificationi (CAV) . 398\u2013414.","DOI":"10.1007\/978-3-319-21690-4_23"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Rishabh Singh and Armando Solar-Lezama. 2011. Synthesizing Data Structure Manipulations from Storyboards. In Foundations of Software Engineeringi (ESEC\/FSE) . 289\u2013299.  Rishabh Singh and Armando Solar-Lezama. 2011. Synthesizing Data Structure Manipulations from Storyboards. In Foundations of Software Engineeringi (ESEC\/FSE) . 289\u2013299.","DOI":"10.1145\/2025113.2025153"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis. In Programming Language Design and Implementation (PLDI) . 326\u2013340.  Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis. In Programming Language Design and Implementation (PLDI) . 326\u2013340.","DOI":"10.1145\/2980983.2908102"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Architectural Support for Programming Languages and Operating Systems (ASPLOS). 404\u2013415.  Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Architectural Support for Programming Languages and Operating Systems (ASPLOS). 404\u2013415.","DOI":"10.1145\/1168917.1168907"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Chenglong Wang Alvin Cheung and Rastislav Bod\u00edk. 2017. Synthesizing Highly Expressive SQL Queries from Input-Output Examples. In Programming Language Design and Implementation (PLDI). 452\u2013466.  Chenglong Wang Alvin Cheung and Rastislav Bod\u00edk. 2017. Synthesizing Highly Expressive SQL Queries from Input-Output Examples. In Programming Language Design and Implementation (PLDI). 452\u2013466.","DOI":"10.1145\/3140587.3062365"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276525"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Jie Zhang Junjie Chen Dan Hao Yingfei Xiong Bing Xie Lu Zhang and Hong Mei. 2014. Search-based Inference of Polynomial Metamorphic Relations. In Automated Software Engineering (ASE). 701\u2013712.  Jie Zhang Junjie Chen Dan Hao Yingfei Xiong Bing Xie Lu Zhang and Hong Mei. 2014. Search-based Inference of Polynomial Metamorphic Relations. In Automated Software Engineering (ASE). 701\u2013712.","DOI":"10.1145\/2642937.2642994"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371124","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371124","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371124","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371124"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":34,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371124"],"URL":"https:\/\/doi.org\/10.1145\/3371124","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}