{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:20:52Z","timestamp":1760059252103,"version":"build-2065373602"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-SHF 2321680"],"award-info":[{"award-number":["CCF-SHF 2321680"]}],"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,10,9]]},"abstract":"<jats:p>Property-based testing (PBT) is a popular technique for automatically testing semantic properties of a program, specified as a pair of pre- and post-conditions. The efficacy of this approach depends on being able to quickly generate inputs that meet the precondition, in order to maximize the set of program behaviors that are probed. For semantically rich preconditions, purely random generation is unlikely to produce many valid inputs; when this occurs, users are forced to manually write their own specialized input generators. One common problem with handwritten generators is that they may be incomplete, i.e., they are unable to generate some values meeting the target precondition. This paper presents a novel program repair technique that patches an incomplete generator so that its range includes every valid input. Our approach uses a novel enumerative synthesis algorithm that leverages the recently developed notion of coverage types to characterize the set of missing test values as well as the coverage provided by candidate repairs. We have implemented a repair tool for OCaml generators, called Cobb, and used it to repair a suite of benchmarks drawn from the PBT literature.<\/jats:p>","DOI":"10.1145\/3763158","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3008-3036","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["We\u2019ve Got You Covered: Type-Guided Repair of Incomplete Input Generators"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4470-3174","authenticated-orcid":false,"given":"Patrick","family":"LaFontaine","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-7501","authenticated-orcid":false,"given":"Zhe","family":"Zhou","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0513-3107","authenticated-orcid":false,"given":"Ashish","family":"Mishra","sequence":"additional","affiliation":[{"name":"IIT Hyderabad, Kandi, India"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2424","authenticated-orcid":false,"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6261","authenticated-orcid":false,"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 25th International Conference on Computer Aided Verification -","volume":"8044","author":"Albarghouthi Aws","year":"2013","unstructured":"Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044 (CAV 2013). Springer-Verlag, Berlin, Heidelberg. 934\u2013950. isbn:9783642397981"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. In 2013 Formal Methods in Computer-Aided Design. 1\u20138. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"volume-title":"Synthesis Through Unification","author":"Alur Rajeev","key":"e_1_2_1_3_1","unstructured":"Rajeev Alur, Pavol \u010cern\u00fd, and Arjun Radhakrishna. 2015. Synthesis Through Unification. In Computer Aided Verification, Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). Springer International Publishing, Cham. 163\u2013179. isbn:978-3-319-21668-3"},{"key":"e_1_2_1_4_1","unstructured":"Daneshvar Amrollahi Mathias Preiner Aina Niemetz Andrew Reynolds Moses Charikar Cesare Tinelli and Clark Barrett. 2025. Towards SMT Solver Stability via Input Normalization. arxiv:2410.22419. arxiv:2410.22419"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428295"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428295"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571226"},{"key":"e_1_2_1_9_1","unstructured":"Koen Claessen. 2020. QuickCheck. https:\/\/hackage.haskell.org\/package\/QuickCheck"},{"key":"e_1_2_1_10_1","volume-title":"Pa\u0142 ka","author":"Claessen Koen","year":"2014","unstructured":"Koen Claessen, Jonas Dureg\u00e5rd, and Micha\u0142 H. Pa\u0142 ka. 2014. Generating Constrained Random\u00a0Data with\u00a0Uniform\u00a0Distribution. In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing, Cham. 18\u201334. isbn:978-3-319-07151-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364515"},{"key":"e_1_2_1_15_1","unstructured":"2022. fast-check: Property based testing for JavaScript and TypeScript. https:\/\/dubzzz.github.io\/fast-check.github.com\/"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837629"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 46th ACM\/IEEE International Conference on Software Engineering (ICSE \u201924)","author":"Goldstein Harrison","year":"2024","unstructured":"Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head. 2024. Property-Based Testing in Practice. In Proceedings of the 46th ACM\/IEEE International Conference on Software Engineering (ICSE \u201924). Association for Computing Machinery, New York, NY, USA."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3654777.3676407"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836091"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371080"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_2_1_26_1","unstructured":"2022. Hypothesis. https:\/\/github.com\/HypothesisWorks\/hypothesis\/tree\/master\/hypothesis-python"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428273"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Patrick LaFontaine Zhe Zhou Ashish Mishra Benjamin Delaware and Suresh Jagannathan. 2025. We\u2019ve Got You Covered: Type-Guided Repair of Incomplete Input Generators. arxiv:2504.06421.","DOI":"10.1145\/3763158"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Patrick LaFontaine Zhe Zhou Ashish Mishra Benjamin Delaware and Suresh Jagannathan. 2025. We\u2019ve Got You Covered: Type-Guided Repair of Incomplete Input Generators. https:\/\/doi.org\/10.5281\/zenodo.16599071 10.5281\/zenodo.16599071","DOI":"10.5281\/zenodo.16599071"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_1_34_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2022","unstructured":"Leonidas Lampropoulos and Benjamin C. Pierce. 2022. QuickChick: Property-Based Testing in Coq (Software Foundations, Vol. 4). Electronic textbook. Version 1.3.1, https:\/\/softwarefoundations.cis.upenn.edu"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106309"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2022.3183091"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571263"},{"key":"e_1_2_1_39_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my KC Sivaramakrishnan and J\u00e9r\u00f4me Vouillon. 2024. The OCaml system release 5.2: Documentation and user\u2019s manual. Ph. D. Dissertation. Inria."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384626"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1979.234198"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.48"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498682"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563310"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/AST.2019.00013"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242744.3242747"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.244.7"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486890"},{"key":"e_1_2_1_50_1","volume-title":"BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=yHeg4PbFHh","author":"Odena Augustus","year":"2021","unstructured":"Augustus Odena, Kensen Shi, David Bieber, Rishabh Singh, Charles Sutton, and Hanjun Dai. 2021. BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration. In International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=yHeg4PbFHh"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523707"},{"key":"e_1_2_1_55_1","volume-title":"Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998)","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998). Springer-Verlag, Berlin, Heidelberg. 151\u2013166. isbn:3540643567"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591292"},{"key":"e_1_2_1_59_1","unstructured":"2024. QCheck. https:\/\/c-cube.github.io\/qcheck\/"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485535"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380399"},{"key":"e_1_2_1_62_1","unstructured":"2020. Rigorous Engineering of Mainstream Systems. https:\/\/www.cl.cam.ac.uk\/ pes20\/rems\/index_introduction.html"},{"key":"e_1_2_1_63_1","unstructured":"2021. Crate for PBT in Rust. https:\/\/github.com\/BurntSushi\/quickcheck"},{"key":"e_1_2_1_64_1","unstructured":"2021. ScalaCheck. https:\/\/scalacheck.org\/"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786825"},{"volume-title":"Program Synthesis by Sketching. Ph. D. Dissertation","author":"Solar-Lezama Armando","key":"e_1_2_1_68_1","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph. D. Dissertation. University of California at Berkeley. USA."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133886"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591255"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591271"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763158","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763158","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:43:39Z","timestamp":1760031819000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763158"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":72,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763158"],"URL":"https:\/\/doi.org\/10.1145\/3763158","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}