{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:45Z","timestamp":1767928545610,"version":"3.49.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-19-C-0073"],"award-info":[{"award-number":["HR0011-19-C-0073"]}],"id":[{"id":"10.13039\/100000185","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,6,6]]},"abstract":"<jats:p>Test input generators are an important part of property-based testing (PBT) frameworks. Because PBT is intended to test deep semantic and structural properties of a program, the outputs produced by these generators can be complex data structures, constrained to satisfy properties the developer believes is most relevant to testing the function of interest. An important feature expected of these generators is that they be capable of producing<jats:italic>all<\/jats:italic>acceptable elements that satisfy the function\u2019s input type and generator-provided constraints. However, it is not readily apparent how we might validate whether a particular generator\u2019s output satisfies this<jats:italic>coverage<\/jats:italic>requirement. Typically, developers must rely on manual inspection and post-mortem analysis of test runs to determine if the generator is providing sufficient coverage; these approaches are error-prone and difficult to scale as generators become more complex. To address this important concern, we present a new refinement type-based verification procedure for validating the coverage provided by input test generators, based on a novel interpretation of types that embeds \u201c<jats:italic>must<\/jats:italic>-style\u201d underapproximate reasoning principles as a fundamental part of the type system. The types associated with expressions now capture the set of values<jats:italic>guaranteed<\/jats:italic>to be produced by the expression, rather than the typical formulation that uses types to represent the set of values an expression<jats:italic>may<\/jats:italic>produce. Beyond formalizing the notion of<jats:italic>coverage types<\/jats:italic>in the context of a rich core language with higher-order procedures and inductive datatypes, we also present a detailed evaluation study to justify the utility of our ideas.<\/jats:p>","DOI":"10.1145\/3591271","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1244-1267","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Covering All the Bases: Type-Based Verification of Test Input Generators"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-7501","authenticated-orcid":false,"given":"Zhe","family":"Zhou","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0513-3107","authenticated-orcid":false,"given":"Ashish","family":"Mishra","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6261","authenticated-orcid":false,"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2424","authenticated-orcid":false,"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133904"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360544"},{"key":"e_1_2_1_3_1","unstructured":"Koen Claessen. 2020. QuickCheck. https:\/\/hackage.haskell.org\/package\/QuickCheck Koen Claessen. 2020. QuickCheck. https:\/\/hackage.haskell.org\/package\/QuickCheck"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_2"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_2_1_8_1","unstructured":"Stephen Dolan. 2022. Crowbar. https:\/\/github.com\/stedolan\/crowbar Stephen Dolan. 2022. Crowbar. https:\/\/github.com\/stedolan\/crowbar"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_12"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_25"},{"key":"e_1_2_1_12_1","unstructured":"2022. fast-check: Property based testing for JavaScript and TypeScript. https:\/\/dubzzz.github.io\/fast-check.github.com\/ 2022. fast-check: Property based testing for JavaScript and TypeScript. https:\/\/dubzzz.github.io\/fast-check.github.com\/"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473601"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_19_1","unstructured":"2022. Hypothesis. https:\/\/github.com\/HypothesisWorks\/hypothesis\/tree\/master\/hypothesis-python 2022. Hypothesis. https:\/\/github.com\/HypothesisWorks\/hypothesis\/tree\/master\/hypothesis-python"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268973"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_2_1_22_1","volume-title":"Random Testing for Language Design. Ph. D. Dissertation","author":"Lampropoulos Leonidas","unstructured":"Leonidas Lampropoulos . 2018. Random Testing for Language Design. Ph. D. Dissertation . University of Pennsylvania . https:\/\/repository.upenn.edu\/edissertations\/2879 Leonidas Lampropoulos. 2018. Random Testing for Language Design. Ph. D. Dissertation. University of Pennsylvania. https:\/\/repository.upenn.edu\/edissertations\/2879"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009868"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_1_26_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 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_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563310"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.27"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_1_35_1","unstructured":"2021. Crate for PBT in Rust. https:\/\/github.com\/BurntSushi\/quickcheck 2021. Crate for PBT in Rust. https:\/\/github.com\/BurntSushi\/quickcheck"},{"key":"e_1_2_1_36_1","unstructured":"2021. ScalaCheck. https:\/\/scalacheck.org\/ 2021. ScalaCheck. https:\/\/scalacheck.org\/"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628161"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_1_40_1","unstructured":"Michal Zalewski. 2020. American Fuzzy Lop. https:\/\/github.com\/google\/afl Michal Zalewski. 2020. American Fuzzy Lop. https:\/\/github.com\/google\/afl"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485493"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Zhe Zhou Ashish Mishra Benjamin Delaware and Suresh Jagannathan. 2023. Covering All the Bases: Type-Based Verification of Test Input Generators. arxiv:2304.03393. Zhe Zhou Ashish Mishra Benjamin Delaware and Suresh Jagannathan. 2023. Covering All the Bases: Type-Based Verification of Test Input Generators. arxiv:2304.03393.","DOI":"10.1145\/3591271"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7811004"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591271","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591271","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591271"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":43,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591271"],"URL":"https:\/\/doi.org\/10.1145\/3591271","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}