{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:06:50Z","timestamp":1790075210320,"version":"4.0.1"},"reference-count":46,"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"}],"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                    We introduce\n                    <jats:italic toggle=\"yes\">semantic reification,<\/jats:italic>\n                    a novel paradigm for random program generation that centers on program semantics rather than syntax. Our key insight is to reformulate random program generation to capture two types of program semantics: (1) compile-time semantics (what a program can do), represented by the control flow graph (CFG), and (2) runtime semantics (what a program actually does), represented by execution paths within the CFG. For any CFG and any execution path on it, semantic reification constructs a program guaranteed to be\n                    <jats:italic toggle=\"yes\">well-behaved<\/jats:italic>\n                    with respect to a specific input and output. This means that when executed with this input, the program deterministically follows the designated execution path to produce the expected output. This paradigm differs from existing work by supporting arbitrary control flow such as unbounded loops and irreducible regions, while still ensuring that the generated programs are semantically correct and terminating. We develop a practical realization of this paradigm. First, we introduce\n                    <jats:italic toggle=\"yes\">symbolic function reification<\/jats:italic>\n                    that integrates a lightweight form of symbolic execution into the generation process to generate an individual, leaf function (i.e., a function that is free of function calls). Each leaf function satisfies the constraints of a given CFG and a selected execution path. Second, we compose multiple leaf functions into a larger, more complex program via semantics-preserving peephole rewriting, guided by an arbitrary call graph. Over five months, our implementation for C compilers,\n                    <jats:sc>Reify,<\/jats:sc>\n                    has uncovered 59 bugs in GCC and LLVM (57 confirmed, 27 fixed), 24 of which are long-latent. Among them, 36 are wrong-code bugs, many are high-priority issues, and most of them involve semantic characteristics overlooked by existing tools. We believe semantic reification opens new directions for research beyond compilers, such as validating debuggers, analyzers, and verifiers.\n                  <\/jats:p>","DOI":"10.1145\/3808268","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"531-554","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Semantic Reification: A New Paradigm for Random Program Generation"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-1831-036X","authenticated-orcid":false,"given":"Kavya","family":"Chopra","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9576-100X","authenticated-orcid":false,"given":"Cong","family":"Li","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9906-3073","authenticated-orcid":false,"given":"Thodoris","family":"Sotiropoulos","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2970-1391","authenticated-orcid":false,"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485500"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Stefanos Chaliasos Thodoris Sotiropoulos Diomidis Spinellis Arthur Gervais Benjamin Livshits and Dimitris Mitropoulos. 2022. Finding Typing Compiler Bugs. In Proceedings of the 2022 ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI \u201822). doi:10.1145\/3519939.3523427","DOI":"10.1145\/3519939.3523427"},{"key":"e_1_3_2_4_2","volume-title":"Metamorphic Testing: A New Approach for Generating Next Test Cases","author":"Chen Tsong Yueh","year":"1998","unstructured":"Tsong Yueh Chen, Shing Chi Cheung, and Shiu Ming Yiu. 1998. Metamorphic Testing: A New Approach for Generating Next Test Cases. Department of Computer Science, The Hong Kong University of Science and Technology, Tech. Rep. HKUST-CS98-01 (1998)."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Kavya Chopra Cong Li Thodoris Sotiropoulos and Zhendong Su. 2026. Artifact for Reify: Semantic Reification: A New Paradigm for Random Program Generation. doi:10.5281\/zenodo.19880827","DOI":"10.5281\/zenodo.19880827"},{"key":"e_1_3_2_6_2","unstructured":"cppreference. 2025. Undefined Behavior (C). https:\/\/en.cppreference.com\/w\/c\/language\/behavior.html"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Karine Even-Mendoza Arindam Sharma Alastair F. Donaldson and Cristian Cadar. 2023. GrayC: Greybox Fuzzing of Compilers and Analysers for C. In Proceedings of the 2023 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA \u201823). doi:10.1145\/3597926.3598130","DOI":"10.1145\/3597926.3598130"},{"key":"e_1_3_2_8_2","unstructured":"GCC. 2025. GIMPLE. https:\/\/gcc.gnu.org\/onlinedocs\/gccint\/GIMPLE.html"},{"key":"e_1_3_2_9_2","unstructured":"GCC. 2025. Leaf Functions. https:\/\/gcc.gnu.org\/onlinedocs\/gccint\/Leaf-Functions.html"},{"key":"e_1_3_2_10_2","unstructured":"GCC. 2025. Passes and Files of the Compiler. https:\/\/gcc.gnu.org\/onlinedocs\/gccint\/Passes.html"},{"key":"e_1_3_2_11_2","volume-title":"FuzzIL: Coverage Guided Fuzzing for JavaScript Engines","author":"Gro\u00df Samuel","year":"2018","unstructured":"Samuel Gro\u00df. 2018. FuzzIL: Coverage Guided Fuzzing for JavaScript Engines. Master\u2019s thesis. Karlsruhe Institute of Technology."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani. 2011. Automating String Processing in Spreadsheets using Input-Output Examples. In Proceedings of the 2011 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201811). doi:10.1145\/1925844.1926423","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_3_2_13_2","unstructured":"Mohammad R. Haghighat Dmitry Khukhro Andrey Yakovlev Nina Rinskaya and Ivan Popov. 2018. JavaFuzzer. https:\/\/github.com\/AzulSystems\/JavaFuzzer"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/911909"},{"key":"e_1_3_2_15_2","unstructured":"Christian Holler Kim Herzig and Andreas Zeller. 2012. Fuzzing with Code Fragments. In Proceedings of the 2012 USENIX Conference on Security Symposium (Security \u201812)."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Timotej Kapus and Cristian Cadar. 2019. A Segmented Memory Model for Symbolic Execution. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE \u201819). doi:10.1145\/3338906.3338936","DOI":"10.1145\/3338906.3338936"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19 (1976). doi:10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729275"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Seungwan Kwon Jaeseong Kwon Wooseok Kang Juneyoung Lee and Kihong Heo. 2024. Translation Validation for JIT Compiler in the V8 JavaScript Engine. In Proceedings of the 2024 IEEE\/ACM 46th International Conference on Software Engineering (ICSE \u201824). doi:10.1145\/3597503.3639189","DOI":"10.1145\/3597503.3639189"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler Validation via Equivalence modulo Inputs. In Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201814). doi:10.1145\/2666356.2594334","DOI":"10.1145\/2666356.2594334"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Vu Le Chengnian Sun and Zhendong Su. 2015. Finding Deep Compiler Bugs via Guided Stochastic Program Mutation. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA \u201815). doi:10.1145\/2814270.2814319","DOI":"10.1145\/2814270.2814319"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM 52 (2009). doi:10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656386"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527317"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Vsevolod Livinskii Dmitry Babokin and John Regehr. 2023. Fuzzing Loop Optimizations in Compilers for C++ and Data-Parallel Languages. Proc. ACM Program. Lang. PLDI (2023). doi:10.1145\/3591295","DOI":"10.1145\/3591295"},{"key":"e_1_3_2_27_2","unstructured":"LLVM. 2025. LLVM Language Reference Manual. https:\/\/llvm.org\/docs\/LangRef.html"},{"key":"e_1_3_2_28_2","unstructured":"LLVM. 2025. LLVM\u2019s Analysis and Transform Passes. https:\/\/llvm.org\/docs\/Passes.html"},{"issue":"1","key":"e_1_3_2_29_2","article-title":"Differential Testing for Software","volume":"10","author":"McKeeman William M.","year":"1998","unstructured":"William M. McKeeman. 1998. Differential Testing for Software. Digit. Tech. J. 10, 1 (1998).","journal-title":"Digit. Tech. J."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Eriko Nagai Atsushi Hashimoto and Nagisa Ishiura. 2014. Reinforcing Random Testing of Arithmetic Optimization of C Compilers by Scaling up Size and Number of Expressions. IPSJ Trans. Syst. LSI Des. Methodol. 7 (2014). doi:10.2197\/ipsjtsldm.7.91","DOI":"10.2197\/ipsjtsldm.7.91"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"George C. Necula. 2000. Translation Validation for An Optimizing Compiler. In Proceedings of the 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201800). doi:10.1145\/358438.349314","DOI":"10.1145\/358438.349314"},{"key":"e_1_3_2_32_2","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","year":"2004","unstructured":"Flemming Nielson, Hanne R Nielson, and Chris Hankin. 2004. Principles of Program Analysis. Springer Science & Business Media."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Xianfei Ou Cong Li Yanyan Jiang and Chang Xu. 2024. The Mutators Reloaded: Fuzzing Compilers with Large Language Model Generated Mutation Operators. In Proceedings of the 2024 ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS \u201824). doi:10.1145\/3622781.3674171","DOI":"10.1145\/3622781.3674171"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"John Regehr Yang Chen Pascal Cuoq Eric Eide Chucky Ellison and Xuejun Yang. 2012. Test-Case Reduction for C Compiler Bugs. In Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201812). doi:10.1145\/2254064.2254104","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Yuyang Rong Zhanghan Yu Zhenkai Weng Stephen Neuendorffer and Hao Chen. 2025. IRFuzzer: Specialized Fuzzing for LLVM Backend Code Generation. In Proceedings of the 2025 IEEE\/ACM International Conference on Software Engineering (ICSE \u201825). doi:10.1109\/icse55347.2025.00130","DOI":"10.1109\/icse55347.2025.00130"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Mayank Sharma Pingshi Yu and Alastair F. Donaldson. 2023. RustSmith: Random Differential Compiler Testing for Rust. In Proceedings of the 2023 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA \u201823). doi:10.1145\/3597926.3604919","DOI":"10.1145\/3597926.3604919"},{"key":"e_1_3_2_37_2","volume-title":"Program Synthesis by Sketching","author":"Solar-Lezama Armando","year":"2008","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. Advisor(s) Bodik, Rastislav."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632904"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Chengnian Sun Vu Le and Zhendong Su. 2016. Finding Compiler Bugs via Live Code Mutation. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA \u201816). doi:10.1145\/2983990.2984038","DOI":"10.1145\/2983990.2984038"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Chengnian Sun Vu Le Qirun Zhang and Zhendong Su. 2016. Toward Understanding Compiler Bugs in GCC and LLVM. In Proceedings of the 2016 International Symposium on Software Testing and Analysis (ISSTA \u201816). doi:10.1145\/2931037.2931074","DOI":"10.1145\/2931037.2931074"},{"key":"e_1_3_2_41_2","unstructured":"V8. 2025. Land Ahoy: Leaving the Sea of Nodes. https:\/\/v8.dev\/blog\/leaving-the-sea-of-nodes"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3763094"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689780"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Elaine J. Weyuker. 1982. On Testing Non-Testable Programs. Comput. J. 25 (1982). doi:10.1093\/comjnl\/25.4.465","DOI":"10.1093\/comjnl\/25.4.465"},{"key":"e_1_3_2_45_2","volume-title":"Translation Validation for the HotSpot C2 Just-in-Time Compiler","author":"Wu Zhiyuan","year":"2025","unstructured":"Zhiyuan Wu. 2025. Translation Validation for the HotSpot C2 Just-in-Time Compiler. Master\u2019s thesis. KTH Royal Institute of Technology."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and Understanding Bugs in C Compilers. In Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201811). doi:10.1145\/1993316.1993532","DOI":"10.1145\/1993316.1993532"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Qirun Zhang Chengnian Sun and Zhendong Su. 2017. Skeletal Program Enumeration for Rigorous Compiler Testing. In Proceedings of the 2017 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI \u201817). doi:10.1145\/3140587.3062379","DOI":"10.1145\/3140587.3062379"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:45:11Z","timestamp":1790073911000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808268"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":46,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808268"],"URL":"https:\/\/doi.org\/10.1145\/3808268","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","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"}}]}}