{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T06:18:08Z","timestamp":1784182688167,"version":"3.55.0"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030393212","type":"print"},{"value":"9783030393229","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-39322-9_3","type":"book-chapter","created":{"date-parts":[[2020,1,14]],"date-time":"2020-01-14T19:03:59Z","timestamp":1579028639000},"page":"44-67","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Fixing Code that Explodes Under Symbolic Evaluation"],"prefix":"10.1007","author":[{"given":"Sorawee","family":"Porncharoenwase","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"Bornholt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,1,13]]},"reference":[{"key":"3_CR1","unstructured":"The RISC-V Instruction Set Manual, Volume II: Privileged Architecture. RISC-V Foundation, June 2019"},{"key":"3_CR2","unstructured":"Amazon Web Services: Quivela (2018). https:\/\/github.com\/awslabs\/quivela"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-17462-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Becker","year":"2019","unstructured":"Becker, N., M\u00fcller, P., Summers, A.J.: The axiom profiler: understanding and debugging SMT quantifier instantiations. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 99\u2013116. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_6"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Kaufmann, A., Li, J., Krishnamurthy, A., Torlak, E., Wang, X.: Specifying and checking file system crash-consistency models. In: Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Atlanta, GA, USA, pp. 83\u201398, April 2016","DOI":"10.1145\/2872362.2872406"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and litmus tests. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Barcelona, Spain, pp. 467\u2013481, June 2017","DOI":"10.1145\/3062341.3062353"},{"key":"3_CR7","first-page":"149:1","volume":"2","author":"J Bornholt","year":"2018","unstructured":"Bornholt, J., Torlak, E.: Finding code that explodes under symbolic evaluation. Proc. ACM Program. Lang. (OOPSLA) 2, 149:1\u2013149:26 (2018)","journal-title":"Proc. ACM Program. Lang. (OOPSLA)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Borning, A.: Wallingford: toward a constraint reactive programming language. In: Proceedings of the Constrained and Reactive Objects Workshop (CROW), M\u00e1laga, Spain, March 2016","DOI":"10.1145\/2892664.2892667"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bucur, S., Kinder, J., Candea, G.: Prototyping symbolic execution engines for interpreted languages. In: Proceedings of the 19th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Salt Lake City, UT, USA , pp. 239\u2013254, March 2014","DOI":"10.1145\/2541940.2541977"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Butler, E., Torlak, E., Popovi\u0107, Z.: Synthesizing interpretable strategies for solving puzzle games. In: Proceedings of the 12th International Conference on the Foundations of Digital Games (FDG), No. 10, Hyannis, MA, USA, August 2017","DOI":"10.1145\/3102071.3102084"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Cadar, C.: Targeted program transformations for symbolic execution. In: Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), Bergamo, Italy, pp. 906\u2013909, August 2015","DOI":"10.1145\/2786805.2803205"},{"issue":"POPL","key":"3_CR12","doi-asserted-by":"publisher","first-page":"62:1","DOI":"10.1145\/3158150","volume":"2","author":"K Chandra","year":"2018","unstructured":"Chandra, K., Bodik, R.: Bonsai: synthesis-based reasoning for type systems. Proc. ACM Program. Lang. 2(POPL), 62:1\u201362:34 (2018)","journal-title":"Proc. ACM Program. Lang."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: S2E: a platform for in-vivo multi-path analysis of software systems. In: Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 265\u2013278 (2011)","DOI":"10.1145\/1961296.1950396"},{"key":"3_CR14","unstructured":"Chu, S., Wang, C., Weitz, K., Cheung, A.: Cosette: an automated prover for SQL. In: Proceedings of the 8th Biennial Conference on Innovative Data Systems (CIDR), Chaminade, CA, USA, January 2017"},{"key":"3_CR15","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR17","first-page":"243","volume-title":"Formal Models and Semantics","author":"Nachum DERSHOWITZ","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.: Rewrite systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 243\u2013320 (1990)"},{"key":"3_CR18","unstructured":"Flatt, M.: PLT: Reference: Racket. Technical report, PLT-TR-2010-1, PLT Design Inc. (2010)"},{"key":"3_CR19","unstructured":"Fleming, M.: A thorough introduction to eBPF, December 2017. https:\/\/lwn.net\/Articles\/740157\/"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Gal, A., et al.: Trace-based just-in-time type specialization for dynamic languages. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 465\u2013478, June 2009","DOI":"10.1145\/1542476.1542528"},{"key":"3_CR21","unstructured":"Galois Inc: Crucible (2018). https:\/\/github.com\/GaloisInc\/crucible"},{"key":"3_CR22","unstructured":"Gill, A.J., Jones, S.L.P.: Cheap deforestation in practice: an optimizer for Haskell. In: IFIP Congress (1994)"},{"key":"3_CR23","volume-title":"The Compiler Design Handbook","author":"Rajiv Gupta","year":"2002","unstructured":"Gupta, R., Mehofer, E., Zhang, Y.: Profile guided compiler optimizations (chap. 4). In: The Compiler Design Handbook: Optimizations and Machine Code Generation. CRC Press, September 2002"},{"key":"3_CR24","unstructured":"Intel Corporation: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. Intel Corporation (2015). Revision 53"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-73721-8_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Kazerounian","year":"2018","unstructured":"Kazerounian, M., Vazou, N., Bourgerie, A., Foster, J.S., Torlak, E.: Refinement types for ruby. In: Dillig, I., Palsberg, J., et al. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 269\u2013290. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_13"},{"issue":"7","key":"3_CR26","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Beijing, China, pp. 89\u201398, June 2012","DOI":"10.1145\/2254064.2254088"},{"key":"3_CR28","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO), Palo Alto, California, March 2004"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., Wang, X.: Scaling symbolic evaluation for automated verification of systems code with Serval. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), pp. 225\u2013242 (2019)","DOI":"10.1145\/3341301.3359641"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Nelson, L., et al.: Hyperkernel: push-button verification of an OS kernel. In: Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pp. 252\u2013269 (2017)","DOI":"10.1145\/3132747.3132748"},{"key":"3_CR31","unstructured":"Newcomb, J.L., Bodik, R.: Using human-in-the-loop synthesis to author functional reactive programs (2019)"},{"key":"3_CR32","unstructured":"Paleczny, M., Vick, C., Click, C.: The Java HotSpot server compiler. In: Proceedings of the 2001 Symposium on Java Virtual Machine Research and Technology (JVM), Monterey, CA, USA, April 2001"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-41540-6_2","volume-title":"Computer Aided Verification","author":"S Pernsteiner","year":"2016","unstructured":"Pernsteiner, S., Loncaric, C., Torlak, E., Tatlock, Z., Wang, X., Ernst, M.D., Jacky, J.: Investigating safety of a radiotherapy machine using system models with pluggable checkers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 23\u201341. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_2"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Pettis, K., Hansen, R.C.: Profile guided code positioning. In: Proceedings of the 11th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), White Plains, NY, USA, pp. 16\u201327, June 1990","DOI":"10.1145\/93548.93550"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Phothilimthana, P.M., et al.: Swizzle inventor: data movement synthesis for GPU kernels. In: Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 65\u201378 (2019)","DOI":"10.1145\/3297858.3304059"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. In: Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Atlanta, GA, USA, pp. 297\u2013310, April 2016","DOI":"10.1145\/2954680.2872387"},{"key":"3_CR37","unstructured":"Racket: The Racket Programming Language (2017). https:\/\/racket-lang.org"},{"key":"3_CR38","unstructured":"S2E: S2E: exponential analysis speedup with state merging (2019). http:\/\/s2e.systems\/docs\/StateMerging.html"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Sen, K., Kalasapur, S., Brutch, T., Gibbs, S.: Jalangi: a selective record-replay and dynamic analysis framework for JavaScript. In: Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE), Saint Petersburg, Russian Federation, pp. 488\u2013498, August 2013","DOI":"10.1145\/2491411.2491447"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Conditionally correct superoptimization. In: Proceedings of the 30th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, USA, pp. 147\u2013162, October 2015","DOI":"10.1145\/2858965.2814278"},{"key":"3_CR41","unstructured":"Sigurbjarnarson, H., Nelson, L., Castro-Karney, B., Bornholt, J., Torlak, E., Wang, X.: Nickel: a framework for design and verification of information flow control systems. In: Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI), pp. 287\u2013305 (2018)"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"St-Amour, V., Tobin-Hochstadt, S., Felleisen, M.: Optimization coaching: optimizers learn to communicate with programmers. In: Proceedings of the 27th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Tuscon, AZ, USA, pp. 163\u2013178, October 2012","DOI":"10.1145\/2398857.2384629"},{"key":"3_CR43","unstructured":"Torlak, E.: Rosette (2018). http:\/\/github.com\/emina\/rosette"},{"key":"3_CR44","unstructured":"Torlak, E.: The Rosette guide: symbolic reflection (2019). https:\/\/docs.racket-lang.org\/rosette-guide\/ch_symbolic-reflection.html"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: Growing solver-aided languages with Rosette. In: Proceedings of the 2013 ACM Symposium on New Ideas in Programming and Reflections on Software (Onward!), Indianapolis, IN, USA, pp. 135\u2013152, October 2013","DOI":"10.1145\/2509578.2509586"},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Edinburgh, United Kingdom, pp. 530\u2013541, June 2014","DOI":"10.1145\/2594291.2594340"},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Uhler, R., Dave, N.: Smten with satisfiability-based search. In: Proceedings of the 29th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Portland, OR, USA, pp. 157\u2013176, October 2014","DOI":"10.1145\/2714064.2660208"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-19027-9_23","volume-title":"ESOP \u201988","author":"P Wadler","year":"1988","unstructured":"Wadler, P.: Deforestation: transforming programs to eliminate trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 344\u2013358. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-19027-9_23"},{"key":"3_CR49","unstructured":"Wagner, J., Kuznetsov, V., Candea, G.: -OVERIFY: optimizing programs for fast verification. In: Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS), Santa Ana Pueblo, NM, USA, May 2013"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Scalable verification of border gateway protocol configurations with an SMT solver. In: Proceedings of the 31st ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Amsterdam, The Netherlands, pp. 765\u2013780, October 2016","DOI":"10.1145\/3022671.2984012"},{"key":"3_CR51","unstructured":"Willsey, M., Ceze, L., Strauss, K.: Puddle: an operating system for reliable, high-level programming of digital microfluidic devices. In: Proceedings of the 23rd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Wild and Crazy Ideas Session, Williamsburg, VA, USA, March 2018"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-39322-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T18:42:57Z","timestamp":1710268977000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-39322-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030393212","9783030393229"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-39322-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"13 January 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Orleans, LA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 January 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2020a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl20.sigplan.org\/home\/VMCAI-2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}