{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:19:51Z","timestamp":1760059191290,"version":"build-2065373602"},"reference-count":89,"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\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-24-C-B044"],"award-info":[{"award-number":["FA8750-24-C-B044"]}],"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":[[2025,10,9]]},"abstract":"<jats:p>\n            Property-based testing (PBT), widely used in functional languages and  \ninteractive theorem provers, works by randomly generating many inputs  \nto a system under test. While PBT has also seen some use in  \nlow-level languages like C, users in this setting must craft  \nall their own generators by hand, rather than letting the tool  \nsynthesize most generators automatically from types or logical  \nspecifications. For low-level code with complex memory ownership  \npatterns, writing such generators can waste significant amounts of  \ntime.  \n  \nCN, a specification and verification framework for C, features a  \nstreamlined presentation of separation logic that is specially tuned  \nto present only \"easy\" logical problems to an underlying constraint  \nsolver. Prior work on the Fulminate testing framework has shown that  \nCN's streamlined specifications can also be checked effectively at run  \ntime, providing an oracle for testing whether a memory state satisfies  \na pre- or postcondition.  \n  \nWe show that the restricted syntax of CN is also a good basis for  \nderiving\n            <jats:italic toggle=\"yes\">generators<\/jats:italic>\n            for random inputs satisfying  \nseparation-logic preconditions. We formalize the semantics for a DSL  \ndescribing these generators, as well as optimizations that reorder  \nwhen values are generated and propagate arithmetic constraints. Using  \nthis DSL, we implement a property-based testing tool, Bennet,  \nthat generates and runs random tests for C functions annotated with CN  \nspecifications. We evaluate Bennet on a corpus of programs with  \nCN specifications and show that it can efficiently generate  \nbug-revealing inputs for heap-manipulating programs with complex  \npreconditions.\n          <\/jats:p>","DOI":"10.1145\/3764115","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3924-3953","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Bennet: Randomized Specification Testing for Heap-Manipulating Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9170-8351","authenticated-orcid":false,"given":"Zain K","family":"Aamer","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7839-1636","authenticated-orcid":false,"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2025. CN. https:\/\/github.com\/rems-project\/cn"},{"key":"e_1_2_1_2_1","unstructured":"2025. libFuzzer. http:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16937824"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1486"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159789.1159792"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23371"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704879"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 28th USENIX Security Symposium. 1985\u20132002","author":"Blazytko Tim","year":"2019","unstructured":"Tim Blazytko, Cornelius Aschermann, Moritz Schl\u00f6gel, Ali Abbasi, Sergej Schumilo, Simon W\u00f6rner, and Thorsten Holz. 2019. GRIMOIRE: Synthesizing Structure while Fuzzing. In Proceedings of the 28th USENIX Security Symposium. 1985\u20132002. isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/blazytko"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837621"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409748"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978428"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, USA. 209\u2013224."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_1_18_1","unstructured":"Mathieu Carlier Catherine Dubois and Arnaud Gotlieb. 2010. Constraint Reasoning in FocalTest. In ICSOFT. https:\/\/inria.hal.science\/hal-00699233"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29578-2_9"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616610"},{"key":"e_1_2_1_21_1","volume-title":"EasyCheck \u2014 Test Data for Free","author":"Christiansen Jan","unstructured":"Jan Christiansen and Sebastian Fischer. 2008. EasyCheck \u2014 Test Data for Free. In Functional and Logic Programming, Jacques Garrigue and Manuel V. Hermenegildo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 322\u2013336. isbn:978-3-540-78969-7"},{"key":"e_1_2_1_22_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 Data with Uniform Distribution. 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_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000143"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_2_1_26_1","volume-title":"14th USENIX Workshop on Offensive Technologies (WOOT 20)","author":"Fioraldi Andrea","year":"2020","unstructured":"Andrea Fioraldi, Dominik Maier, Heiko Ei\u00df feldt, and Marc Heuse. 2020. AFL++ : Combining Incremental Steps of Fuzzing Research. In 14th USENIX Workshop on Offensive Technologies (WOOT 20). https:\/\/www.usenix.org\/conference\/woot20\/presentation\/fioraldi"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00172"},{"key":"e_1_2_1_29_1","unstructured":"Galois Inc. 2025. VERSE-OpenSUT. Github. https:\/\/github.com\/GaloisInc\/VERSE-OpenSUT"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607842"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563291"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2009.10"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510228"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464795"},{"key":"e_1_2_1_38_1","volume-title":"Trends in Functional Programming, William J","author":"Hughes John","unstructured":"John Hughes. 2020. How to Specify It!. In Trends in Functional Programming, William J. Bowman and Ronald Garcia (Eds.). Springer International Publishing, Cham. 58\u201383. isbn:978-3-030-47147-7"},{"key":"e_1_2_1_39_1","volume-title":"Pierce","author":"Hughes John","year":"2024","unstructured":"John Hughes, Rini Banerjee, and Benjamin C. Pierce. 2024. Adventures in Specification-Based Testing. Invited talk at Isaac Newton Institute Workshop on Big Specification: Specification, Proof, and Testing at Scale"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243804"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_1_45_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018","unstructured":"Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickChick: Property-Based Testing in Coq. https:\/\/softwarefoundations.cis.upenn.edu\/qc-current\/ Electronic textbook"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122959"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238176"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230636"},{"key":"e_1_2_1_50_1","first-page":"105","article-title":"Property Directed Generation of First-Order Test Data","volume":"8","author":"Lindblad Fredrik","year":"2007","unstructured":"Fredrik Lindblad. 2007. Property Directed Generation of First-Order Test Data.. Trends in Functional Programming, 8 (2007), 105\u2013123.","journal-title":"Trends in Functional Programming"},{"key":"e_1_2_1_51_1","volume-title":"MOPT: Optimized Mutation Scheduling for Fuzzers. In 28th USENIX Security Symposium (USENIX Security 19)","author":"Lyu Chenyang","year":"2019","unstructured":"Chenyang Lyu, Shouling Ji, Chao Zhang, Yuwei Li, Wei-Han Lee, Yu Song, and Raheem Beyah. 2019. MOPT: Optimized Mutation Scheduling for Fuzzers. In 28th USENIX Security Symposium (USENIX Security 19). 1949\u20131966. isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/lyu"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30634-6_4"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.13"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.21105\/joss.01891"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/272991.272995"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion52605.2021.00053"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/AST.2019.00013"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST57152.2023.00025"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3299711.3242747"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_62_1","unstructured":"Rickard Nilsson. 2024. ScalaCheck. https:\/\/scalacheck.org\/."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/369534.369540"},{"key":"e_1_2_1_64_1","volume-title":"Random Testing in PVS. In Workshop on Automated Formal Methods (AFM). 10","author":"Owre Sam","year":"2006","unstructured":"Sam Owre. 2006. Random Testing in PVS. In Workshop on Automated Formal Methods (AFM). 10, Seattle."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3339002"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034654.2034663"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523707"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_27"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3194964"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_12"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2941681"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_2_1_75_1","volume-title":"CN tutorial. https:\/\/rems-project.github.io\/cn-tutorial\/ [Online","author":"Pulte Christopher","year":"2024","unstructured":"Christopher Pulte, Benjamin C. Pierce, Cole Schlesinger, and Elizabeth Austell. 2024. CN tutorial. https:\/\/rems-project.github.io\/cn-tutorial\/ [Online; accessed 26-October-2024]"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3654440"},{"key":"e_1_2_1_77_1","volume-title":"Quickly Generating Diverse Valid Test Inputs with Reinforcement Learning. In 2020 IEEE\/ACM 42nd International Conference on Software Engineering (ICSE). 1410\u20131421","author":"Reddy Sameer","year":"2020","unstructured":"Sameer Reddy, Caroline Lemieux, Rohan Padhye, and Koushik Sen. 2020. Quickly Generating Diverse Valid Test Inputs with Reinforcement Learning. In 2020 IEEE\/ACM 42nd International Conference on Software Engineering (ICSE). 1410\u20131421. issn:1558-1225 https:\/\/ieeexplore.ieee.org\/document\/9284117"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3604921"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00239"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607860"},{"key":"e_1_2_1_84_1","unstructured":"Stephen Dolan and Mindy Preston. 2017. Testing with Crowbar. https:\/\/github.com\/ocaml\/ocaml.org-media\/blob\/master\/meetings\/ocaml\/2017\/extended-abstract__2017__stephen-dolan_mindy-preston__testing-with-crowbar.pdf"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80691-1"},{"key":"e_1_2_1_86_1","unstructured":"Scott Vokes. 2019. theft: property-based testing for C. https:\/\/github.com\/silentbicycle\/theft"},{"key":"e_1_2_1_87_1","unstructured":"Jinghan Wang Yue Duan Wei Song Heng Yin and Chengyu Song. 2019. Be Sensitive and Collaborative: Analyzing Impact of Coverage Metrics in Greybox Fuzzing. 1\u201315. isbn:978-1-939133-07-6 https:\/\/www.usenix.org\/conference\/raid2019\/presentation\/wang"},{"key":"e_1_2_1_88_1","unstructured":"Micha\u0142 Zalewski. 2017. American Fuzzy Lop. http:\/\/lcamtuf.coredump.cx\/afl\/"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632911"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764115","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:42:13Z","timestamp":1760031733000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":89,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3764115"],"URL":"https:\/\/doi.org\/10.1145\/3764115","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}