{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:04Z","timestamp":1751660524055,"version":"3.41.0"},"reference-count":87,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Facebook"},{"DOI":"10.13039\/100016682","name":"VMware","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100016682","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science Foundation","award":["1553471, 1564207, 1918483, 1910216"],"award-info":[{"award-number":["1553471, 1564207, 1918483, 1910216"]}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100011735","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0018050"],"award-info":[{"award-number":["DE-SC0018050"]}],"id":[{"id":"10.13039\/100011735","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":[[2020,11,13]]},"abstract":"<jats:p>Building effective symbolic execution engines poses challenges in multiple dimensions: an engine must correctly model the program semantics, provide flexibility in symbolic execution strategies, and execute them efficiently.<\/jats:p>\n          <jats:p>This paper proposes a principled approach to building correct, flexible, and efficient symbolic execution engines, directly rooted in the semantics of the underlying language in terms of a high-level definitional interpreter. The definitional interpreter induces algebraic effects to abstract over semantic variants of symbolic execution, e.g., collecting path conditions as a state effect and path exploration as a nondeterminism effect. Different handlers of these effects give rise to different symbolic execution strategies, making execution strategies orthogonal to the symbolic execution semantics, thus improving flexibility. Furthermore, by annotating the symbolic definitional interpreter with binding-times and specializing it to the input program via the first Futamura projection, we obtain a \"symbolic compiler\", generating efficient instrumented code having the symbolic execution semantics. Our work reconciles the interpretation- and instrumentation-based approaches to building symbolic execution engines in a uniform framework.<\/jats:p>\n          <jats:p>We illustrate our approach on a simple imperative language step-by-step and then scale up to a significant subset of LLVM IR. We also show effect handlers for common path selection strategies. Evaluating our prototype's performance shows speedups of 10~30x over the unstaged counterpart, and ~2x over KLEE, a state-of-the-art symbolic interpreter for LLVM IR.<\/jats:p>","DOI":"10.1145\/3428232","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:40:14Z","timestamp":1606261214000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Compiling symbolic execution with staging and algebraic effects"],"prefix":"10.1145","volume":"4","author":[{"given":"Guannan","family":"Wei","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oliver","family":"Bra\u010devac","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shangyin","family":"Tan","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2426890.2426917"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009867"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158140"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Anand Saswat","key":"e_1_2_2_4_1","unstructured":"Saswat Anand , Corina S. P\u0103s\u0103reanu , and Willem Visser . 2007. JPF-SE: A Symbolic Execution Extension to Java PathFinder . In Tools and Algorithms for the Construction and Analysis of Systems , Orna Grumberg and Michael Huth (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 134-138. Saswat Anand, Corina S. P\u0103s\u0103reanu, and Willem Visser. 2007. JPF-SE: A Symbolic Execution Extension to Java PathFinder. In Tools and Algorithms for the Construction and Analysis of Systems, Orna Grumberg and Michael Huth (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 134-138."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_2_6_1","first-page":"4","volume-title":"Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation","author":"Bawden Alan","year":"1999","unstructured":"Alan Bawden . 1999 . Quasiquotation in Lisp . In Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation , San Antonio, Texas, USA , January 22-23, 1999. Technical report BRICS-NS-99-1, Olivier Danvy (Ed.). University of Aarhus, 4 - 12 . Alan Bawden. 1999. Quasiquotation in Lisp. In Proceedings of the 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, San Antonio, Texas, USA, January 22-23, 1999. Technical report BRICS-NS-99-1, Olivier Danvy (Ed.). University of Aarhus, 4-12."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61053-7_62"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236762"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56039-4_38"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541977"},{"key":"e_1_2_2_12_1","volume-title":"CREST: Concolic test generation tool for C.","author":"Burnim Jacob","year":"2014","unstructured":"Jacob Burnim . 2014 . CREST: Concolic test generation tool for C. Jacob Burnim. 2014. CREST: Concolic test generation tool for C."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110252"},{"key":"e_1_2_2_15_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation","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 ( San Diego, California) ( OSDI'08). USENIX Association, USA , 209 - 224 . 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 (San Diego, California) ( OSDI'08). USENIX Association, USA, 209-224."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39815-8_4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"volume-title":"Theoretical Aspects of Computer Software, Masami Hagiya and John C","author":"Cartwright Robert","key":"e_1_2_2_20_1","unstructured":"Robert Cartwright and Matthias Felleisen . 1994. Extensible denotational language specifications . In Theoretical Aspects of Computer Software, Masami Hagiya and John C . Mitchell (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 244-272. Robert Cartwright and Matthias Felleisen. 1994. Extensible denotational language specifications. In Theoretical Aspects of Computer Software, Masami Hagiya and John C. Mitchell (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 244-272."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/DagRep.8.4.104"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950396"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/202530.202534"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110256"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89719-6_6"},{"key":"e_1_2_2_27_1","volume-title":"Flare: Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018","author":"Essertel Gr\u00e9gory M.","year":"2018","unstructured":"Gr\u00e9gory M. Essertel , Ruby Y. Tahboub , James M. Decker , Kevin J. Brown , Kunle Olukotun , and Tiark Rompf . 2018 . Flare: Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018 , Carlsbad, CA, USA , October 8-10, 2018., Andrea C. Arpaci-Dusseau and Geof Voelker (Eds.). USENIX Association, 799-815. https:\/\/www.usenix.org\/conference\/osdi18\/ presentation\/essertel Gr\u00e9gory M. Essertel, Ruby Y. Tahboub, James M. Decker, Kevin J. Brown, Kunle Olukotun, and Tiark Rompf. 2018. Flare: Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018., Andrea C. Arpaci-Dusseau and Geof Voelker (Eds.). USENIX Association, 799-815. https:\/\/www.usenix.org\/conference\/osdi18\/ presentation\/essertel"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291178"},{"volume-title":"The Reasoned Schemer","author":"Friedman Daniel P.","key":"e_1_2_2_31_1","unstructured":"Daniel P. Friedman , William E. Byrd , Oleg Kiselyov , and Jason Hemann . 2018. The Reasoned Schemer , Second Edition. MIT Press . Daniel P. Friedman, William E. Byrd, Oleg Kiselyov, and Jason Hemann. 2018. The Reasoned Schemer, Second Edition. MIT Press."},{"key":"e_1_2_2_32_1","first-page":"348","volume-title":"Proceedings of the 1984 ACM Conference on LISP and Functional Programming, LFP 1984","author":"Daniel","year":"1984","unstructured":"Daniel P. Friedman and Mitchell Wand. 1984. Reification: Reflection without Metaphysics . In Proceedings of the 1984 ACM Conference on LISP and Functional Programming, LFP 1984 , August 5-8, 1984 , Austin, Texas, USA. ACM , 348 - 355 . Daniel P. Friedman and Mitchell Wand. 1984. Reification: Reflection without Metaphysics. In Proceedings of the 1984 ACM Conference on LISP and Functional Programming, LFP 1984, August 5-8, 1984, Austin, Texas, USA. ACM, 348-355."},{"key":"e_1_2_2_33_1","first-page":"45","volume-title":"Computers, Controls 25 ( 1971 )","author":"Futamura Yoshihiko","unstructured":"Yoshihiko Futamura . 1971. Partial evaluation of computation process-an approach to a compiler-compiler. Systems , Computers, Controls 25 ( 1971 ) , 45 - 50 . Yoshihiko Futamura. 1971. Partial evaluation of computation process-an approach to a compiler-compiler. Systems, Computers, Controls 25 ( 1971 ), 45-50."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010095604496"},{"key":"e_1_2_2_35_1","volume-title":"Dill","author":"Ganesh Vijay","year":"2007","unstructured":"Vijay Ganesh and David L . Dill . 2007 . A Decision Procedure for Bit-Vectors and Arrays. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 519-531. Vijay Ganesh and David L. Dill. 2007. A Decision Procedure for Bit-Vectors and Arrays. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 519-531."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_22"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.18"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449913.1449935"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.231144"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500604"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158139"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90091-1"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16446-4_11"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90006-X"},{"volume-title":"Two-level Functional Languages","author":"Nielson Flemming","key":"e_1_2_2_49_1","unstructured":"Flemming Nielson and Hanne Riis Nielson . 1992. Two-level Functional Languages . Cambridge University Press , New York, NY, USA . Flemming Nielson and Hanne Riis Nielson. 1992. Two-level Functional Languages. Cambridge University Press, New York, NY, USA."},{"volume-title":"Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science )","author":"Nielson Hanne Riis","key":"e_1_2_2_50_1","unstructured":"Hanne Riis Nielson and Flemming Nielson . 2007. Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science ) . Springer-Verlag , Berlin, Heidelberg . Hanne Riis Nielson and Flemming Nielson. 2007. Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science ). Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136040.3136060"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517208.2517228"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000106"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_2_57_1","first-page":"181","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon . 2020 . Symbolic execution with SymCC: Don't interpret, compile! . In 29th USENIX Security Symposium (USENIX Security 20) . USENIX Association , 181 - 198 . https:\/\/www.usenix.org\/conference\/ usenixsecurity20\/presentation\/poeplau Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. Symbolic execution with SymCC: Don't interpret, compile!. In 29th USENIX Security Symposium (USENIX Security 20). USENIX Association, 181-198. https:\/\/www.usenix.org\/conference\/ usenixsecurity20\/presentation\/poeplau"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110260"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_17"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784760"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-013-9096-9"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.238"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596596"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868314"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2245276.2231988"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178068"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357765.3359514"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278122.3278139"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259019"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3196893"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318464.3389701"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3315507.3330200"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360552"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236800"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/bs.adcom.2018.10.002"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360563"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428232","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428232","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428232","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428232"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":87,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428232"],"URL":"https:\/\/doi.org\/10.1145\/3428232","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}