{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T00:39:24Z","timestamp":1790987964696,"version":"4.1.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"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-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":[[2026,6,8]]},"abstract":"<jats:p>\n                    Several recently proposed program logics have incorporated notions of\n                    <jats:italic toggle=\"yes\">under approximation<\/jats:italic>\n                    into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an expressive type and effect system. We use the resulting underapproximate type specifications to guide the synthesis of test generators that probe the behavior of effectful black-box systems. A key novelty of our type language is its ability to capture underapproximate behaviors of\n                    <jats:italic toggle=\"yes\">effectful<\/jats:italic>\n                    operations using symbolic traces that expose latent data and control dependencies, constraints that must be preserved by the test sequences the generator outputs. We implement this approach in a tool called Clouseau, and evaluate it on a diverse range of applications by integrating Clouseau\u2019s synthesized generators into property-based testing frameworks like QCheck and model-checking tools like P. In both settings, the generators synthesized by Clouseau are significantly more effective than the default testing strategy, and are competitive with state-of-the-art, handwritten solutions.\n                  <\/jats:p>","DOI":"10.1145\/3808264","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"430-454","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Trace-Guided Synthesis of Effectful Test Generators"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-7501","authenticated-orcid":false,"given":"Zhe","family":"Zhou","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9006-0100","authenticated-orcid":false,"given":"Ankush","family":"Desai","sequence":"additional","affiliation":[{"name":"Snowflake, San Mateo, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6261","authenticated-orcid":false,"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2424","authenticated-orcid":false,"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485546"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706339"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Cristiano Calcagno and Dino Distefano. 2011. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In Proceedings of the Third International Conference on NASA Formal Methods (Pasadena CA) (NFM\u201911). Springer-Verlag Berlin Heidelberg 459\u2013465. doi:10.1007\/978-3-642-20398-5_33","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","unstructured":"Maria Christakis Alkis Gotovos and Konstantinos Sagonas. 2013. Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In 2013 IEEE Sixth International Conference on Software Testing Verification and Validation. 154\u2013163. doi:10.1109\/ICST.2013.50","DOI":"10.1109\/ICST.2013.50"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1631687.1596574"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535849"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_1_11_2","first-page":"854","volume-title":"Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (Beijing, China) (IJCAI \u201913)","author":"De Giacomo Giuseppe","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence (Beijing, China) (IJCAI \u201913). AAAI Press, 854\u2013860. https:\/\/dl.acm.org\/doi\/10.5555\/2540128.2540252"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276529"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_1"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.14778\/2732240.2732246"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632919"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","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 IEEE\/ACM International Conference on Software Engineering ICSE 2024 Lisbon Portugal April 14-20 2024. ACM 187:1\u2013187:13. doi:10.1145\/3597503.3639581","DOI":"10.1145\/3597503.3639581"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500574"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_17"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603138"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763158"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3776724"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3759427.3760378"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Anders Miltner Saswat Padhi Todd D. Millstein and David Walker. 2020. Data-driven Inference of Representation Invariants. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation PLDI. ACM 1\u201315. doi:10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622876"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523728"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_3_1_36_2","unstructured":"QCheck 2024. QuickCheck Inspired Property-Based Testing for OCaml. https:\/\/c-cube.github.io\/qcheck\/"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2023.25"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632909"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4842-8_1"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689745"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Zhe Zhou Ankush Desai Benjamin Delaware and Suresh Jagannathan. 2026. Trace-Guided Synthesis of Effectful Test Generators. arXiv:2604.04345 [cs.PL] doi:10.48550\/arXiv.2604.04345","DOI":"10.48550\/arXiv.2604.04345"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591271"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Zhe Zhou John Rose Rebekah Sowards and Aadi Rave. 2026. PLDI26 Artifact: Trace-Guided Synthesis of Effectful Test Generators. doi:10.5281\/zenodo.19076511","DOI":"10.5281\/zenodo.19076511"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656433"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808264","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:44:00Z","timestamp":1790073840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808264"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":48,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808264"],"URL":"https:\/\/doi.org\/10.1145\/3808264","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}