{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T16:26:40Z","timestamp":1761582400947,"version":"build-2065373602"},"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\/"}],"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\n            <jats:italic toggle=\"yes\">size-bounded<\/jats:italic>\n            synthesis functions,    which extends our completeness result    to an infinite set of possible specifications.    In particular, we describe a size-bounded synthesis function    for linear integer arithmetic constraints.    We conclude with an evaluation demonstrating our technique on a variety of benchmarks.                                                                                                                    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\n            <jats:italic toggle=\"yes\">size-bounded<\/jats:italic>\n            synthesis functions,                                                                                                                                which extends our completeness result                                                                                                                                to an infinite set of possible specifications.                                                                                                                                In particular, we describe a size-bounded 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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3267-0776","authenticated-orcid":false,"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837628"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314641"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2018.00074"},{"key":"e_1_2_2_6_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. 8, 209\u2013224.","journal-title":"OSDI."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2009. Generalized efficient array decision procedures. In 2009 Formal Methods in Computer-Aided Design. 45\u201352. https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142 10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509511"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276501"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0267-5"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","unstructured":"William T. Hallahan Ranjit Jhala and Ruzica Piskac. 2025. Lynx. https:\/\/doi.org\/10.5281\/zenodo.14942480 10.5281\/zenodo.14942480","DOI":"10.5281\/zenodo.14942480"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314618"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360592"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_18"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385979"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737987"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542485"},{"key":"e_1_2_2_29_1","volume-title":"Proc. 5th Berkeley Symp. Math. Stat. Probab.","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).."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062372"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106281"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155662"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/232629.232636"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622861"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_31"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426900"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998533"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192416"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858949.2784766"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","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":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:14:58Z","timestamp":1760030098000},"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":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}