{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:22Z","timestamp":1784200222557,"version":"3.55.0"},"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>Property-based testing (PBT), widely used in functional languages and interactive theorem provers, works by randomly generating many inputs to a system under test. While PBT has also seen some use in low-level languages like C, users in this setting must craft all their own generators by hand, rather than letting the tool synthesize most generators automatically from types or logical specifications. For low-level code with complex memory ownership patterns, writing such generators can waste significant amounts of time.<\/jats:p>\n                  <jats:p>CN, a specification and verification framework for C, features a streamlined presentation of separation logic that is specially tuned to present only \u201ceasy\u201d logical problems to an underlying constraint solver. Prior work on the Fulminate testing framework has shown that CN\u2019s streamlined specifications can also be checked effectively at run time, providing an oracle for testing whether a memory state satisfies a pre-or postcondition.<\/jats:p>\n                  <jats:p>\n                    We show that the restricted syntax of CN is also a good basis for deriving\n                    <jats:italic toggle=\"yes\">generators<\/jats:italic>\n                    for random inputs satisfying separation-logic preconditions. We formalize the semantics for a DSL describing these generators, as well as optimizations that reorder when values are generated and propagate arithmetic constraints. Using this DSL, we implement a property-based testing tool, Bennet, that generates and runs random tests for C functions annotated with CN specifications. We evaluate Bennet on a corpus of programs with CN specifications and show that it can efficiently generate bug-revealing inputs for heap-manipulating programs with complex preconditions.\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":2,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"2025. CN. https:\/\/github.com\/rems-project\/cn"},{"key":"e_1_3_1_3_2","unstructured":"2025. libFuzzer. http:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Zain K Aamer and Benjamin C. Pierce. 2025. Artifact for Bennet: Randomized Specification Testing for Heap-Manipulating Programs. Zenodo. doi:10.5281\/zenodo.16937824","DOI":"10.5281\/zenodo.16937824"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1486"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1159789.1159792"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23371"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704879"},{"key":"e_1_3_1_11_2","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. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/blazytko"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837621"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409748"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978428"},{"key":"e_1_3_1_16_2","first-page":"209","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_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_1_19_2","unstructured":"Mathieu Carlier Catherine Dubois and Arnaud Gotlieb. 2010. Constraint Reasoning in FocalTest. In ICSOFT. https:\/\/inria.hal.science\/hal-00699233"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29578-2_9"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616610"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78969-7_23"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_2"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000143"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_3_1_27_2","unstructured":"Andrea Fioraldi Dominik Maier Heiko Ei\u00dffeldt 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_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00172"},{"key":"e_1_3_1_30_2","unstructured":"Galois Inc. 2025. VERSE-OpenSUT. Github. https:\/\/github.com\/GaloisInc\/VERSE-OpenSUT"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607842"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563291"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Arnaud Gotlieb. 2009. Euclide: A Constraint-Based Testing Framework for Critical C Programs. In 2009 International Conference on Software Testing Verification and Validation. 151\u2013160. doi:10.1109\/ICST.2009.10","DOI":"10.1109\/ICST.2009.10"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510228"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464795"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-47147-7_4"},{"key":"e_1_3_1_40_2","article-title":"Adventures in Specification-Based Testing","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.","journal-title":"Invited talk at Isaac Newton Institute Workshop on Big Specification: Specification, Proof, and Testing at Scale"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243804"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360607"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_3_1_46_2","unstructured":"Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickChick: Property-Based Testing in Coq. https:\/\/softwarefoundations.cis.upenn.edu\/qc-current\/ Electronictextbook."},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122959"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_26"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238176"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3230636"},{"key":"e_1_3_1_51_2","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_3_1_52_2","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. https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/lyu"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30634-6_4"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.13"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.21105\/joss.01891"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/272991.272995"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","unstructured":"Agust\u00edn Mista. 2021. MUTAGEN: Faster Mutation-Based Random Testing. In 2021 IEEE\/ACM 43rd International Conference on Software Engineering: Companion Proceedings (ICSE-Companion). 120\u2013122. doi:10.1109\/ICSE-Companion52605.2021.00053 ISSN: 2574-1926.","DOI":"10.1109\/ICSE-Companion52605.2021.00053"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","unstructured":"Agust\u00edn Mista and Alejandro Russo. 2019. Generating Random Structurally Rich Algebraic Data Type Values. In 2019 IEEE\/ACM 14th International Workshop on Automation of Software Test (AST). IEEE 48\u201354. doi:10.1109\/AST.2019.00013","DOI":"10.1109\/AST.2019.00013"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","unstructured":"Agust\u00edn Mista and Alejandro Russo. 2023. MUTAGEN: Reliable Coverage-Guided Property-Based Testing using Exhaustive Mutations. In 2023 IEEE Conference on Software Testing Verification and Validation (ICST). 176\u2013187. doi:10.1109\/ICST57152.2023.00025 ISSN: 2159-4848.","DOI":"10.1109\/ICST57152.2023.00025"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3299711.3242747"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_63_2","unstructured":"Rickard Nilsson. 2024. ScalaCheck. https:\/\/scalacheck.org\/."},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/369534.369540"},{"key":"e_1_3_1_65_2","volume-title":"Workshop on Automated Formal Methods (AFM)","author":"Owre Sam","year":"2006","unstructured":"Sam Owre. 2006. Random Testing in PVS. In Workshop on Automated Formal Methods (AFM), Vol. 10. Seattle."},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3339002"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034654.2034663"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523707"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_27"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3194964"},{"key":"e_1_3_1_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_12"},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2941681"},{"key":"e_1_3_1_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_3_1_76_2","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_3_1_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3654440"},{"key":"e_1_3_1_78_2","doi-asserted-by":"crossref","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. https:\/\/ieeexplore.ieee.org\/document\/9284117","DOI":"10.1145\/3377811.3380399"},{"key":"e_1_3_1_79_2","doi-asserted-by":"publisher","unstructured":"J.C. Reynolds. 2002. Separation logic: a logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. 55\u201374. doi:10.1109\/LICS.2002.1029817 ISSN: 1043-6871.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_80_2","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3604921"},{"key":"e_1_3_1_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_3_1_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_3_1_83_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00239"},{"key":"e_1_3_1_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607860"},{"key":"e_1_3_1_85_2","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_3_1_86_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80691-1"},{"key":"e_1_3_1_87_2","unstructured":"Scott Vokes. 2019. theft: property-based testing for C. https:\/\/github.com\/silentbicycle\/theft"},{"key":"e_1_3_1_88_2","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. https:\/\/www.usenix.org\/conference\/raid2019\/presentation\/wang"},{"key":"e_1_3_1_89_2","unstructured":"Micha\u0142 Zalewski. 2017. American Fuzzy Lop. http:\/\/lcamtuf.coredump.cx\/afl\/"},{"key":"e_1_3_1_90_2","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":[[2026,7,16]],"date-time":"2026-07-16T10:14:30Z","timestamp":1784196870000},"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"}}]}}