{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T05:50:46Z","timestamp":1770270646008,"version":"3.49.0"},"reference-count":49,"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":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1750965, CCF-1763871, CCF-1918211, CCF-2023222, CCF-2211968, CCF-2212558"],"award-info":[{"award-number":["CCF-1750965, CCF-1763871, CCF-1918211, CCF-2023222, CCF-2211968, CCF-2212558"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2889"],"award-info":[{"award-number":["N00014-17-1-2889"]}],"id":[{"id":"10.13039\/100000006","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":"<jats:p>Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: i) a query posed about a set of function definitions, and ii) a domain-specific language L in which the extracted property is to be expressed (we call properties in the language L-properties). Each of the property is a best L-property for the query: there is no other L-property that is strictly more precise. Furthermore, the set of synthesized L-properties is exhaustive: no more L-properties can be added to it to make the conjunction more precise.  \nWe implemented our method in a tool, Spyro. The ability to modify both the query and L provides a Spyro user with ways to customize the kind of specification to be synthesized. We use this ability to show that Spyro can be used in a variety of applications, such as mining program specifications, performing abstract-domain operations, and synthesizing algebraic properties of program modules.<\/jats:p>","DOI":"10.1145\/3622861","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"1787-1816","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Synthesizing Specifications"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-7983-233X","authenticated-orcid":false,"given":"Kanghee","family":"Park","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D'Antoni","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"#cr-split#-e_1_2_1_1_1.1","unstructured":"Rajeev Alur Dana Fisman Saswat Padhi Rishabh Singh and Abhishek Udupa. 2019. SyGuS-Comp 2018: Results and Analysis. https:\/\/doi.org\/10.48550\/ARXIV.1904.07146 10.48550\/ARXIV.1904.07146"},{"key":"#cr-split#-e_1_2_1_1_1.2","unstructured":"Rajeev Alur Dana Fisman Saswat Padhi Rishabh Singh and Abhishek Udupa. 2019. SyGuS-Comp 2018: Results and Analysis. https:\/\/doi.org\/10.48550\/ARXIV.1904.07146"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485481"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.49"},{"key":"e_1_2_1_6_1","volume-title":"Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium (USENIX Security 17)","author":"Blazytko Tim","year":"2017","unstructured":"Tim Blazytko , Moritz Contag , Cornelius Aschermann , and Thorsten Holz . 2017 . Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium (USENIX Security 17) . USENIX Association, Vancouver, BC. 643\u2013659. isbn:978-1-93 1971-40-9 https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/blazytko Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC. 643\u2013659. isbn:978-1-931971-40-9 https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/blazytko"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_8_1","unstructured":"Patrick Cousot and Radhia Cousot. 1978. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Descriptions of Programming Concepts. North-Holland. \t\t\t\t  Patrick Cousot and Radhia Cousot. 1978. Static Determination of Dynamic Properties of Recursive Procedures. In Formal Descriptions of Programming Concepts. North-Holland."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505351.2505353"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254087"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_10"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In SAS. \t\t\t\t  Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In SAS.","DOI":"10.1007\/978-3-662-48288-9_12"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_2_1_18_1","volume-title":"Automatic Reasoning for Pointer Programs Using Decidable Logics. Ph. D. Dissertation","author":"Itzhaky Shachar","unstructured":"Shachar Itzhaky . 2014. Automatic Reasoning for Pointer Programs Using Decidable Logics. Ph. D. Dissertation . Tel Aviv University . Shachar Itzhaky. 2014. Automatic Reasoning for Pointer Programs Using Decidable Logics. Ph. D. Dissertation. Tel Aviv University."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774587"},{"key":"e_1_2_1_21_1","unstructured":"Jinwoo Kim. 2022. Messy-Release. https:\/\/github.com\/kjw227\/Messy-Release \t\t\t\t  Jinwoo Kim. 2022. Messy-Release. https:\/\/github.com\/kjw227\/Messy-Release"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434311"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.149.2"},{"key":"e_1_2_1_24_1","volume-title":"David Lo, Siau-Cheng Khoo","unstructured":"2017. Mining Software Specifications: Methodologies and Applications , David Lo, Siau-Cheng Khoo , Jiawei Han, and Chao Liu (Eds.). Chapman & Hall . 2017. Mining Software Specifications: Methodologies and Applications, David Lo, Siau-Cheng Khoo, Jiawei Han, and Chao Liu (Eds.). Chapman & Hall."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360558"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_2_1_27_1","volume-title":"Machine Learning","author":"Mitchell Tom M.","unstructured":"Tom M. Mitchell . 1997. Machine Learning . McGraw-Hill . Tom M. Mitchell. 1997. Machine Learning. McGraw-Hill."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_24"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_30_1","volume-title":"Deductive Verification of Distributed Protocols in First-Order Logic. Ph. D. Dissertation","author":"Padon Oded","unstructured":"Oded Padon . 2018. Deductive Verification of Distributed Protocols in First-Order Logic. Ph. D. Dissertation . Tel Aviv University . Oded Padon. 2018. Deductive Verification of Distributed Protocols in First-Order Logic. Ph. D. Dissertation. Tel Aviv University."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498712"},{"key":"e_1_2_1_32_1","unstructured":"Kanghee Park Loris D\u2019Antoni and Thomas Reps. 2023. Synthesizing Specifications. arxiv:2301.11117. \t\t\t\t  Kanghee Park Loris D\u2019Antoni and Thomas Reps. 2023. Synthesizing Specifications. arxiv:2301.11117."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8327699"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_39_1","volume-title":"Program Flow Analysis: Theory and Applications","author":"Sharir Micha","unstructured":"Micha Sharir and Amir Pnueli . 1981. Two Approaches to Interprocedural Data Flow Analysis . In Program Flow Analysis: Theory and Applications . Prentice-Hall . Micha Sharir and Amir Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000090"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_1_45_1","article-title":"Learning with Differential Privacy: Stability, Learnability and the Sufficiency and Necessity of ERM Principle","volume":"17","author":"Wang Yu-Xiang","year":"2016","unstructured":"Yu-Xiang Wang , Jing Lei , and Stephen E. Fienberg . 2016 . Learning with Differential Privacy: Stability, Learnability and the Sufficiency and Necessity of ERM Principle . J. Mach. Learn. Res. , 17 , 1 (2016), jan, 6353\u20136392. issn:1532-4435 Yu-Xiang Wang, Jing Lei, and Stephen E. Fienberg. 2016. Learning with Differential Privacy: Stability, Learnability and the Sufficiency and Necessity of ERM Principle. J. Mach. Learn. Res., 17, 1 (2016), jan, 6353\u20136392. issn:1532-4435","journal-title":"J. Mach. Learn. Res."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485495"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622861","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622861","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622861"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":49,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622861"],"URL":"https:\/\/doi.org\/10.1145\/3622861","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"}}]}}