{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:26:56Z","timestamp":1787592416389,"version":"build-2736575974"},"reference-count":49,"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":[{"name":"NSF","award":["CCF-2219995"],"award-info":[{"award-number":["CCF-2219995"]}]},{"name":"Amazon","award":["The Spring 2021 Amazon Research Award"],"award-info":[{"award-number":["The Spring 2021 Amazon Research Award"]}]}],"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                    Modular verification tools allow programmers to compositionally specify and prove function specifications. When using a modular verifier, proving a specification about a function\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    requires additional specifications for the functions called by\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    . With existing state of the art tools, programmers must manually write the specifications for callee functions. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. We show that if each of these three components is sound and complete over a finite set of possible specifications, our algorithm is sound and complete as well. Additionally, we introduce size-bounded synthesis functions, which extends our completeness result to an infinite set of possible specifications. In particular, we describe a\n                    <jats:italic toggle=\"yes\">size-bounded<\/jats:italic>\n                    synthesis function for linear integer arithmetic constraints. We conclude with an evaluation demonstrating our technique on a variety of benchmarks.\n                  <\/jats:p>","DOI":"10.1145\/3720505","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1689-1716","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Counterexample-Guided Inference of Modular Specifications"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4925-3861","authenticated-orcid":false,"given":"William T.","family":"Hallahan","sequence":"first","affiliation":[{"name":"Binghamton University, Binghamton, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-0776","authenticated-orcid":false,"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837628"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2018.00074"},{"key":"e_1_3_2_7_1","first-page":"209","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.","volume":"8","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In OSDI, Vol. 8. 209\u2013224.","journal-title":"OSDI"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno Dino Distefano Peter O\u2019Hearn and Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 289\u2013300. doi:10.1145\/1480881.1480917","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0267-5"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"William T. Hallahan Ranjit Jhala and Ruzica Piskac. 2025. Lynx. (2025). doi:10.5281\/zenodo.14942480","DOI":"10.5281\/zenodo.14942480"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314618"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360592"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"Qinheping Hu John Cyphert Loris D\u2019Antoni and Thomas Reps. 2020. Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 1128\u20131142. doi:10.1145\/3385412.3385979","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi Ryosuke Sato and Hiroshi Unno. 2011. Predicate abstraction and CEGAR for higher-order model checking. In Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation. 222\u2013233. doi:10.1145\/1993498.1993525","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737987"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542485"},{"key":"e_1_3_2_30_1","first-page":"281","article-title":"Some methods for classification and analysis of multivariate observations","volume":"1","author":"MacQueen J.","year":"1967","unstructured":"J. MacQueen. 1967. Some methods for classification and analysis of multivariate observations. Proc. 5th Berkeley Symp. Math. Stat. Probab., Univ. Calif. 1965\/66, 1, 281-297 (1967).","journal-title":"Proc. 5th Berkeley Symp. Math. Stat. Probab., Univ. Calif. 1965\/66"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155662"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/232629.232636"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622861"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Sumanth Prabhu Grigory Fedyukovich Kumar Madhukar and Deepak D\u2019Souza. 2021. Specification synthesis with constrained Horn clauses. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 1203\u20131217. doi:10.1145\/3453483.3454104","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_31"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","unstructured":"Ryosuke Sato Hiroshi Unno and Naoki Kobayashi. 2013. Towards a scalable software model checker for higher-order programs. In Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation. 53\u201362. doi:10.1145\/2426890.2426900","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998533"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858949.2784766"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","unstructured":"He Zhu Gustavo Petri and Suresh Jagannathan. 2016. Automatically learning shape specifications. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. 491\u2013507. doi:10.1145\/2908080.2908125","DOI":"10.1145\/2908080.2908125"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720505","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720505","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:32:27Z","timestamp":1787589147000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720505"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":49,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720505"],"URL":"https:\/\/doi.org\/10.1145\/3720505","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"}}]}}