{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T19:04:45Z","timestamp":1732043085415},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF #2146518, #2124431, and #2107261"],"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":[[2023,10,16]]},"abstract":"\n The traditional formulation of the program synthesis problem is to find a program that meets a logical correctness specification. When synthesis is successful, there is a guarantee that the implementation satisfies the specification. Unfortunately, synthesis engines are typically monolithic algorithms, and obscure the correspondence between the specification, implementation and user intent. In contrast, humans often include comments in their code to guide future developers towards the purpose and design of different parts of the codebase. In this paper, we introduce\n subspecifications<\/jats:italic>\n as a mechanism to augment the synthesized implementation with explanatory notes of this form. In this model, the user may ask for explanations of different parts of the implementation; the subspecification generated in response is a logical formula that describes the constraints induced on that subexpression by the global specification and surrounding implementation. We develop algorithms to construct and verify subspecifications and investigate their theoretical properties. We perform an experimental evaluation of the subspecification generation procedure, and measure its effectiveness and running time. Finally, we conduct a user study to determine whether subspecifications are useful: we find that subspecifications greatly aid in understanding the global specification, in identifying alternative implementations, and in debugging faulty implementations.\n <\/jats:p>","DOI":"10.1145\/3622874","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"2171-2195","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Explainable Program Synthesis by Localizing Specifications"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"http:\/\/orcid.org\/0009-0000-5675-247X","authenticated-orcid":false,"given":"Amirmohammad","family":"Nazari","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}]},{"ORCID":"http:\/\/orcid.org\/0009-0006-5675-4065","authenticated-orcid":false,"given":"Yifei","family":"Huang","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}]},{"ORCID":"http:\/\/orcid.org\/0009-0000-2456-217X","authenticated-orcid":false,"given":"Roopsha","family":"Samanta","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, IN, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-5559-5932","authenticated-orcid":false,"given":"Arjun","family":"Radhakrishna","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, WA, USA"}]},{"ORCID":"http:\/\/orcid.org\/0000-0003-2879-0932","authenticated-orcid":false,"given":"Mukund","family":"Raghothaman","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-1994-7104"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2870052"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI). AAAI Press","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur , Loris D\u2019Antoni , Sumit Gulwani , Dileep Kini , and Mahesh Viswanathan . 2013 . Automated Grading of DFA Constructions . In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI). AAAI Press , 1976\u20131982. isbn:9781577356332 Rajeev Alur, Loris D\u2019Antoni, Sumit Gulwani, Dileep Kini, and Mahesh Viswanathan. 2013. Automated Grading of DFA Constructions. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI). AAAI Press, 1976\u20131982. isbn:9781577356332"},{"key":"e_1_2_2_5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Alur Rajeev","unstructured":"Rajeev Alur , Arjun Radhakrishna , and Abhishek Udupa . 2017. Scaling Enumerative Program Synthesis via Divide and Conquer . In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . Springer , 319\u2013336. isbn:978-3-662-54577-5 Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 319\u2013336. isbn:978-3-662-54577-5"},{"key":"e_1_2_2_6_1","unstructured":"Solon Barocas Moritz Hardt and Arvind Narayanan. 2019. Fairness and Machine Learning: Limitations and Opportunities. fairmlbook.org. http:\/\/www.fairmlbook.org \t\t\t\t Solon Barocas Moritz Hardt and Arvind Narayanan. 2019. Fairness and Machine Learning: Limitations and Opportunities. fairmlbook.org. http:\/\/www.fairmlbook.org"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106740"},{"key":"e_1_2_2_8_1","volume-title":"Proceedings of the 25th International Conference on Software Engineering (ICSE). IEEE Computer Society, 385\u2013395","author":"Chaki Sagar","year":"2003","unstructured":"Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , and Helmut Veith . 2003 . Modular Verification of Software Components in C . In Proceedings of the 25th International Conference on Software Engineering (ICSE). IEEE Computer Society, 385\u2013395 . isbn:076951877X Sagar Chaki, Edmund Clarke, Alex Groce, Somesh Jha, and Helmut Veith. 2003. Modular Verification of Software Components in C. In Proceedings of the 25th International Conference on Software Engineering (ICSE). IEEE Computer Society, 385\u2013395. isbn:076951877X"},{"key":"e_1_2_2_9_1","unstructured":"Mark Chen Jerry Tworek Heewoo Jun Qiming Yuan Henrique Ponde de Oliveira Pinto Jared Kaplan Harri Edwards Yuri Burda Nicholas Joseph Greg Brockman Alex Ray Raul Puri Gretchen Krueger Michael Petrov Heidy Khlaaf Girish Sastry Pamela Mishkin Brooke Chan Scott Gray Nick Ryder Mikhail Pavlov Alethea Power Lukasz Kaiser Mohammad Bavarian Clemens Winter Philippe Tillet Felipe Petroski Such Dave Cummings Matthias Plappert Fotios Chantzis Elizabeth Barnes Ariel Herbert-Voss William Hebgen Guss Alex Nichol Alex Paino Nikolas Tezak Jie Tang Igor Babuschkin Suchir Balaji Shantanu Jain William Saunders Christopher Hesse Andrew N. Carr Jan Leike Josh Achiam Vedant Misra Evan Morikawa Alec Radford Matthew Knight Miles Brundage Mira Murati Katie Mayer Peter Welinder Bob McGrew Dario Amodei Sam McCandlish Ilya Sutskever and Wojciech Zaremba. 2021. Evaluating Large Language Models Trained on Code. arxiv:2107.03374. \t\t\t\t Mark Chen Jerry Tworek Heewoo Jun Qiming Yuan Henrique Ponde de Oliveira Pinto Jared Kaplan Harri Edwards Yuri Burda Nicholas Joseph Greg Brockman Alex Ray Raul Puri Gretchen Krueger Michael Petrov Heidy Khlaaf Girish Sastry Pamela Mishkin Brooke Chan Scott Gray Nick Ryder Mikhail Pavlov Alethea Power Lukasz Kaiser Mohammad Bavarian Clemens Winter Philippe Tillet Felipe Petroski Such Dave Cummings Matthias Plappert Fotios Chantzis Elizabeth Barnes Ariel Herbert-Voss William Hebgen Guss Alex Nichol Alex Paino Nikolas Tezak Jie Tang Igor Babuschkin Suchir Balaji Shantanu Jain William Saunders Christopher Hesse Andrew N. Carr Jan Leike Josh Achiam Vedant Misra Evan Morikawa Alec Radford Matthew Knight Miles Brundage Mira Murati Katie Mayer Peter Welinder Bob McGrew Dario Amodei Sam McCandlish Ilya Sutskever and Wojciech Zaremba. 2021. Evaluating Large Language Models Trained on Code. arxiv:2107.03374."},{"key":"#cr-split#-e_1_2_2_10_1.1","unstructured":"Finale Doshi-Velez and Been Kim. 2017. Towards A Rigorous Science of Interpretable Machine Learning. https:\/\/doi.org\/10.48550\/ARXIV.1702.08608 arxiv:1702.08608. 10.48550\/ARXIV.1702.08608"},{"key":"#cr-split#-e_1_2_2_10_1.2","unstructured":"Finale Doshi-Velez and Been Kim. 2017. Towards A Rigorous Science of Interpretable Machine Learning. https:\/\/doi.org\/10.48550\/ARXIV.1702.08608 arxiv:1702.08608."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454080"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6943189"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3379337.3415869"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_2_2_16_1","volume-title":"NASA Formal Methods","author":"Finkbeiner Bernd","unstructured":"Bernd Finkbeiner , Gideon Geier , and Noemi Passing . 2021. Specification Decomposition for Reactive Synthesis . In NASA Formal Methods . Springer , 113\u2013130. isbn:978-3-030-76384-8 Bernd Finkbeiner, Gideon Geier, and Noemi Passing. 2021. Specification Decomposition for Reactive Synthesis. In NASA Formal Methods. Springer, 113\u2013130. isbn:978-3-030-76384-8"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRE.1994.292398"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC \/ FSE). ACM, 87\u201398","author":"Handa Shivam","year":"2020","unstructured":"Shivam Handa and Martin Rinard . 2020 . Inductive Program Synthesis over Noisy Data . In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC \/ FSE). ACM, 87\u201398 . isbn:9781450370431 Shivam Handa and Martin Rinard. 2020. Inductive Program Synthesis over Noisy Data. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC \/ FSE). ACM, 87\u201398. isbn:9781450370431"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/985692.985712"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.229.9"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594333"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807442.2807459"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the 33rd International Conference on Neural Information Processing Systems (NeurIPS). Article 1107","author":"Mott Alex","year":"2019","unstructured":"Alex Mott , Daniel Zoran , Mike Chrzanowski , Daan Wierstra , and Danilo Rezende . 2019 . Towards Interpretable Reinforcement Learning Using Attention Augmented Agents . In Proceedings of the 33rd International Conference on Neural Information Processing Systems (NeurIPS). Article 1107 , 10 pages. Alex Mott, Daniel Zoran, Mike Chrzanowski, Daan Wierstra, and Danilo Rezende. 2019. Towards Interpretable Reinforcement Learning Using Attention Augmented Agents. In Proceedings of the 33rd International Conference on Neural Information Processing Systems (NeurIPS). Article 1107, 10 pages."},{"key":"e_1_2_2_28_1","unstructured":"Steven Muchnick. 1998. Advanced Compiler Design and Implementation. Morgan Kaufmann. isbn:1558603204 \t\t\t\t Steven Muchnick. 1998. Advanced Compiler Design and Implementation. Morgan Kaufmann. isbn:1558603204"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8331495"},{"key":"e_1_2_2_30_1","unstructured":"OpenAI. 2022. ChatGPT. https:\/\/openai.com\/blog\/chatgpt\/ \t\t\t\t OpenAI. 2022. ChatGPT. https:\/\/openai.com\/blog\/chatgpt\/"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180189"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_2_35_1","volume-title":"Computer Aided Verification (CAV)","author":"Reynolds Andrew","unstructured":"Andrew Reynolds , Morgan Deters , Viktor Kuncak , Cesare Tinelli , and Clark Barrett . 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT . In Computer Aided Verification (CAV) . Springer , 198\u2013216. isbn:978-3-319-21668-3 Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark Barrett. 2015. Counterexample-Guided Quantifier Instantiation for Synthesis in SMT. In Computer Aided Verification (CAV). Springer, 198\u2013216. isbn:978-3-319-21668-3"},{"key":"#cr-split#-e_1_2_2_36_1.1","unstructured":"Marco Tulio Ribeiro Sameer Singh and Carlos Guestrin. 2016. Model-Agnostic Interpretability of Machine Learning. https:\/\/doi.org\/10.48550\/ARXIV.1606.05386 10.48550\/ARXIV.1606.05386"},{"key":"#cr-split#-e_1_2_2_36_1.2","unstructured":"Marco Tulio Ribeiro Sameer Singh and Carlos Guestrin. 2016. Model-Agnostic Interpretability of Machine Learning. https:\/\/doi.org\/10.48550\/ARXIV.1606.05386"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2939672.2939778"},{"key":"e_1_2_2_38_1","volume-title":"Boon Thau Loo, and Rajeev Alur","author":"Shi Lei","year":"2021","unstructured":"Lei Shi , Yahui Li , Boon Thau Loo, and Rajeev Alur . 2021 . Network Traffic Classification by Program Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer , 430\u2013448. isbn:978-3-030-72016-2 Lei Shi, Yahui Li, Boon Thau Loo, and Rajeev Alur. 2021. Network Traffic Classification by Program Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 430\u2013448. isbn:978-3-030-72016-2"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.14778\/2977797.2977807"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462195"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_2_2_42_1","volume-title":"Information-theoretic User Interaction: Significant Inputs for Program Synthesis. CoRR, abs\/2006.12638","author":"Tiwari Ashish","year":"2020","unstructured":"Ashish Tiwari , Arjun Radhakrishna , Sumit Gulwani , and Daniel Perelman . 2020. Information-theoretic User Interaction: Significant Inputs for Program Synthesis. CoRR, abs\/2006.12638 ( 2020 ), arXiv:2006.12638. arxiv:2006.12638 Ashish Tiwari, Arjun Radhakrishna, Sumit Gulwani, and Daniel Perelman. 2020. Information-theoretic User Interaction: Significant Inputs for Program Synthesis. CoRR, abs\/2006.12638 (2020), arXiv:2006.12638. arxiv:2006.12638"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411764.3445249"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/tvcg.2020.3030418"},{"key":"e_1_2_2_45_1","volume-title":"Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE). IEEE Press, 439\u2013449","author":"Weiser Mark","year":"1981","unstructured":"Mark Weiser . 1981 . Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE). IEEE Press, 439\u2013449 . isbn:0897911466 Mark Weiser. 1981. Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE). IEEE Press, 439\u2013449. isbn:0897911466"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_2_47_1","volume-title":"Proceedings of the 7th European Software Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE). Springer, 253\u2013267","author":"Zeller Andreas","year":"1999","unstructured":"Andreas Zeller . 1999 . Yesterday, My Program Worked. Today, It Does Not. Why? In Proceedings of the 7th European Software Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE). Springer, 253\u2013267 . isbn:3540665382 Andreas Zeller. 1999. Yesterday, My Program Worked. Today, It Does Not. Why? In Proceedings of the 7th European Software Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC\/FSE). Springer, 253\u2013267. isbn:3540665382"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411764.3445646"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3379337.3415900"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2016.319"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622874","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:56:00Z","timestamp":1697471760000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":52,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622874"],"URL":"https:\/\/doi.org\/10.1145\/3622874","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}