{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:23:33Z","timestamp":1787592213585,"version":"build-2736575974"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2422214, CCF-2506134, CCF-2446711"],"award-info":[{"award-number":["CCF-2422214, CCF-2506134, CCF-2446711"]}],"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":[[2025,4,9]]},"abstract":"<jats:p>\n                    This paper tackles the problem of synthesizing specifications for nondeterministic programs. For such programs, useful specifications can capture demonic properties, which hold for\n                    <jats:italic toggle=\"yes\">every<\/jats:italic>\n                    nondeterministic execution, but also angelic properties, which hold for\n                    <jats:italic toggle=\"yes\">some<\/jats:italic>\n                    nondeterministic execution. We build on top of a recently proposed\n                    <jats:sc>spyro<\/jats:sc>\n                    framework in which given (\n                    <jats:italic toggle=\"yes\">i<\/jats:italic>\n                    ) a\n                    <jats:italic toggle=\"yes\">quantifier-free<\/jats:italic>\n                    query \u03a8 posed about a set of function definitions (i.e., the behavior for which we want to generate a specification), and (\n                    <jats:italic toggle=\"yes\">ii<\/jats:italic>\n                    ) a language \u2112 in which each extracted property is to be expressed (we call properties in the language \u2112-properties), the goal is to synthesize a conjunction \u2227\n                    <jats:sub>\ud835\udc56<\/jats:sub>\n                    \ud835\udf11\n                    <jats:sub>\ud835\udc56<\/jats:sub>\n                    of \u2112-properties such that each of the \ud835\udf11\n                    <jats:sub>\ud835\udc56<\/jats:sub>\n                    is a\n                    <jats:italic toggle=\"yes\">strongest<\/jats:italic>\n                    \u2112\n                    <jats:italic toggle=\"yes\">-consequence<\/jats:italic>\n                    for \u03a8: \ud835\udf11\n                    <jats:sub>\ud835\udc56<\/jats:sub>\n                    is an overapproximation of \u03a8 and there is no other \u2112-property that over-approximates \u03a8 and is strictly more precise than \ud835\udf11\n                    <jats:sub>\ud835\udc56<\/jats:sub>\n                    . This framework does not apply to nondeterministic programs for two reasons: it does not support existential quantifiers in queries (which are necessary to expressing nondeterminism) and it can only compute \u2112-consequences, i.e., it is unsuitable for capturing both angelic and demonic properties.\n                  <\/jats:p>\n                  <jats:p>\n                    This paper addresses these two limitations and presents a framework,\n                    <jats:sc>loud<\/jats:sc>\n                    , for synthesizing both\n                    <jats:italic toggle=\"yes\">strongest<\/jats:italic>\n                    \u2112\n                    <jats:italic toggle=\"yes\">-consequences<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">weakest<\/jats:italic>\n                    \u2112\n                    <jats:italic toggle=\"yes\">-implicants<\/jats:italic>\n                    (i.e., under-approximations of the query \u03a8) for queries that can involve\n                    <jats:italic toggle=\"yes\">existential quantifiers<\/jats:italic>\n                    . We devise algorithms for handling the quantifiers appearing in\n                    <jats:sc>loud<\/jats:sc>\n                    queries and implement them in a solver,\n                    <jats:sc>aspire<\/jats:sc>\n                    , for problems expressed in\n                    <jats:sc>loud<\/jats:sc>\n                    which can be used to describe and identify sources of bugs in both deterministic and nondeterministic programs, extract properties from concurrent programs, and synthesize winning strategies in two-player games.\n                  <\/jats:p>","DOI":"10.1145\/3720470","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"956-983","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["LOUD: Synthesizing Strongest and Weakest Specifications"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-7983-233X","authenticated-orcid":false,"given":"Kanghee","family":"Park","sequence":"first","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8613-3506","authenticated-orcid":false,"given":"Xuanyu","family":"Peng","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D'Antoni","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","volume-title":"Operating Systems: Three Easy Pieces","author":"Arpaci-Dusseau Remzi H.","year":"2023","unstructured":"Remzi H. Arpaci-Dusseau and Andrea C. Arpaci-Dusseau. 2023. Operating Systems: Three Easy Pieces (1.10 ed.). Arpaci-Dusseau Books.","edition":"1"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485481"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_15"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.29007\/vv21"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523453"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51074-9_11"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages Los Angeles California USA January 1977 Robert M. Graham Michael A. Harrison and Ravi Sethi (Eds.). ACM 238\u2013252. doi:10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_1_12_2","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. https:\/\/books.google.com\/books?id=MsUmAAAAMAAJ"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926407"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254087"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158149"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190215.1190226"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040316"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_16"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322088"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Pankaj Kumar Kalita Sujit Kumar Muduli Loris D\u2019Antoni Thomas W. Reps and Subhajit Roy. 2022. Synthesizing Abstract Transformers. Proc. ACM Program. Lang. OOPSLA (2022). doi:10.1145\/3563334","DOI":"10.1145\/3563334"},{"key":"e_1_3_1_27_2","unstructured":"Jinwoo Kim. 2022. Messy-Release. https:\/\/github.com\/kjw227\/Messy-Release."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1986002"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31423-1_6"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Kanghee Park. 2025. Loud: Synthesizing Strongest and Weakest Specifications. doi:10.5281\/zenodo.14934344","DOI":"10.5281\/zenodo.14934344"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Kanghee Park Loris D\u2019Antoni and Thomas Reps. 2023. Synthesizing Specifications. 7 OOPSLA2 Article 285 (oct 2023) 30 pages. doi:10.1145\/3622861","DOI":"10.1145\/3622861"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.34727\/2023\/ISBN.978-3-85448-060-0_34"},{"key":"e_1_3_1_37_2","unstructured":"Kanghee Park Xuanyu Peng and Loris D\u2019Antoni. 2024. LOUD: Synthesizing Strongest and Weakest Specifications. arXiv:2408.12539 [cs.PL] https:\/\/arxiv.org\/abs\/2408.12539"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908093"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"ThomasW. Reps Shmuel Sagiv and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In Verification Model Checking and Abstract Interpretation 5th International Conference VMCAI 2004 Venice Italy January 11-13 2004 Proceedings. 252\u2013266. doi:10.1007\/978-3-540-24622-0_21","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.03.008"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000090"},{"key":"e_1_3_1_44_2","unstructured":"Armando Solar-Lezama. 2008. Program synthesis by sketching. Ph.D. Dissertation. USA. Advisor(s) Bodik Rastislav. AAI3353225."},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Aditya V. Thakur Matt Elder and Thomas W. Reps. 2012. Bilateral Algorithms for Symbolic Abstraction. In Static Analysis - 19th International Symposium SAS 2012 Deauville France September 11-13 2012. Proceedings. 111\u2013128. doi:10.1007\/978-3-642-33125-1_10","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Aditya V. Thakur and ThomasW. Reps. 2012. A Method for Symbolic Computation of Abstract Operations. In Computer Aided Verification - 24th International Conference CAV 2012 Berkeley CA USA July 7-13 2012 Proceedings. 174\u2013192. doi:10.1007\/978-3-642-31424-7_17","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2017.2681107"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","unstructured":"S. Zdancewic and A.C. Myers. 2003. Observational determinism for concurrent program security. In 16th IEEE Computer Security Foundations Workshop 2003. Proceedings. 29\u201343. doi:10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_3_1_51_2","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\/3720470","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720470","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720470","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:30:34Z","timestamp":1787589034000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720470"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":50,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720470"],"URL":"https:\/\/doi.org\/10.1145\/3720470","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}