{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T11:09:17Z","timestamp":1778152157541,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":76,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"The Office of Naval Research","award":["N00014-17-1-2996"],"award-info":[{"award-number":["N00014-17-1-2996"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3385964","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"655-671","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Scalable validation of binary lifters"],"prefix":"10.1145","author":[{"given":"Sandeep","family":"Dasgupta","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Sushant","family":"Dinesh","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Deepan","family":"Venkatesh","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Vikram S.","family":"Adve","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Christopher W.","family":"Fletcher","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA."},{"key":"e_1_3_2_1_2_1","volume-title":"https:\/\/rada.re\/r\/. Last accessed","author":"Alvarez Sergi","year":"2020","unstructured":"Sergi Alvarez. 2018. Radare2. https:\/\/rada.re\/r\/. Last accessed: April 20, 2020."},{"key":"e_1_3_2_1_3_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Andriesse Dennis","unstructured":"Dennis Andriesse, Xi Chen, Victor van der Veen, Asia Slowinska, and Herbert Bos. 2016. An In-Depth Analysis of Disassembly on Full-Scale x86\/x64 Binaries. In 25th USENIX Security Symposium (USENIX Security 16). USENIX Association, Austin, TX, 583\u2013 600. https:\/\/www.usenix.org\/conference\/usenixsecurity16\/technicalsessions\/presentation\/andriesse"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628071.2628092"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608"},{"key":"e_1_3_2_1_7_1","unstructured":"1749612"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_13"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1247360.1247401"},{"key":"e_1_3_2_1_10_1","volume-title":"Binary Translator to LLVM IR. https:\/\/github. com\/repzret\/dagger. Last accessed","author":"Bougacha Ahmed","year":"2020","unstructured":"Ahmed Bougacha. 2017. Binary Translator to LLVM IR. https:\/\/github. com\/repzret\/dagger. Last accessed: April 20, 2020."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/776261.776290"},{"key":"e_1_3_2_1_12_1","unstructured":"Derek L. Bruening. 2004. Efficient Transparent and Comprehensive Runtime Code Manipulation. Ph.D. Dissertation. Cambridge MA USA. AAI0807735."},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification","author":"Brumley David","year":"2032","unstructured":"David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J. Schwartz. 2011. BAP: A Binary Analysis Platform. In Proceedings of the 23rd International Conference on Computer Aided Verification (Snowbird, UT) (CAV\u201911). Springer-Verlag, Berlin, Heidelberg, 463\u2013469. http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032342"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.50"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2015.05.002"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSNW.2011.5958815"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.825697"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455820"},{"key":"e_1_3_2_1_21_1","volume-title":"A Scalable Validator for Binary Lifters. https:\/\/github.com\/sdasgup3\/validating-binary-decompilation. Last accessed","author":"Dasgupta Sandeep","year":"2020","unstructured":"Sandeep Dasgupta. 2020. A Scalable Validator for Binary Lifters. https:\/\/github.com\/sdasgup3\/validating-binary-decompilation. Last accessed: April 20, 2020."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"org\/10.1145\/3314221.3314601 10.1145\/3314221.3314601","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3033019.3033028"},{"key":"e_1_3_2_1_26_1","volume-title":"An architecture-independent decompiler to LLVM IR. https:\/\/github.com\/draperlaboratory\/fracture. Last accessed","year":"2020","unstructured":"Draper-Laboratory. [n.d.]. An architecture-independent decompiler to LLVM IR. https:\/\/github.com\/draperlaboratory\/fracture. Last accessed: April 20, 2020."},{"key":"e_1_3_2_1_27_1","volume-title":"Design of a Retargetable Decompiler for a Static Platform-Independent Malware Analysis","author":"\u010eurfina Luk\u00e1\u0161","unstructured":"Luk\u00e1\u0161 \u010eurfina, Jakub K\u0159oustek, Petr Zemek, Du\u0161an Kol\u00e1\u0159, Tom\u00e1\u0161 Hru\u0161ka, Karel Masa\u0159\u00edk, and Alexander Meduna. 2011. Design of a Retargetable Decompiler for a Static Platform-Independent Malware Analysis. In Information Security and Assurance, Tai-hoon Kim, Hojjat Adeli, Rosslin John Robles, and Maricel Balitanas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 72\u201386."},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation","author":"Erlingsson \u00dalfar","unstructured":"\u00dalfar Erlingsson, Mart\u00edn Abadi, Michael Vrable, Mihai Budiu, and George C. Necula. 2006. XFI: Software Guards for System Address Spaces. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (Seattle, Washington) (OSDI \u201906). USENIX Association, Berkeley, CA, USA, 75\u201388. http:\/\/dl.acm.org\/citation. cfm?id=1298455.1298463"},{"key":"e_1_3_2_1_29_1","volume-title":"USENIX 2008 Annual Technical Conference","author":"Ford Bryan","year":"2008","unstructured":"Bryan Ford and Russ Cox. 2008. Vx32: Lightweight User-level Sandboxing on the x86. In USENIX 2008 Annual Technical Conference (Boston, Massachusetts) (ATC\u201908). USENIX Association, Berkeley, CA, USA, 293\u2013306. http:\/\/dl.acm.org\/citation.cfm?id=1404014.1404039"},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of NDSS (Network and Distributed Systems Security). 151\u2013166","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid, Michael Y. Levin, and David Molnar. 2008. Automated Whitebox Fuzz Testing. In Proceedings of NDSS (Network and Distributed Systems Security). 151\u2013166."},{"key":"e_1_3_2_1_31_1","unstructured":"Ilfak Guilfanov. 2008. Decompilers and Beyond. In Black-Hat USA."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127577.1127590"},{"key":"e_1_3_2_1_33_1","volume-title":"Towards Verified Binary Raising. In Workshop on Instruction Set Architecture Specification (co-located with ITP","author":"Hendrix Joe","year":"2019","unstructured":"Joe Hendrix, Guannan Wei, and Simon Winwood. 2019. Towards Verified Binary Raising. In Workshop on Instruction Set Architecture Specification (co-located with ITP 2019)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73573"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.4"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155609"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098954.3103152"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 11th USENIX Security Symposium. USENIX Association","author":"Kiriansky Vladimir","year":"2029","unstructured":"Vladimir Kiriansky, Derek Bruening, and Saman P. Amarasinghe. 2002. Secure Execution via Program Shepherding. In Proceedings of the 11th USENIX Security Symposium. USENIX Association, Berkeley, CA, USA, 191\u2013206. http:\/\/dl.acm.org\/citation.cfm?id=647253.720293"},{"key":"e_1_3_2_1_40_1","volume-title":"Pass the SALT","author":"K\u0159oustek J.","year":"2018","unstructured":"J. K\u0159oustek and P. Matula. 2018. RetDec: An Open-Source Machine-Code Decompiler. [talk]. Presented at Pass the SALT 2018, Lille, FR."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISPASS.2010.5452024"},{"key":"e_1_3_2_1_43_1","first-page":"326357","article-title":"Bochs","volume":"326350","author":"Lawton Kevin P.","year":"1996","unstructured":"Kevin P. Lawton. 1996. Bochs: A Portable PC Emulator for Unix\/X. Linux J. 1996, 29es, Article 7 (Sept. 1996). http:\/\/dl.acm.org\/citation. cfm?id=326350.326357","journal-title":"A Portable PC Emulator for Unix\/X. Linux"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453114"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065034"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.982916"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2151012"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831730"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572303"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2931047"},{"key":"e_1_3_2_1_51_1","volume-title":"Workshop on Instruction Set Architecture Specification (co-located with ITP","author":"Miranti Andrew H.","year":"2019","unstructured":"Andrew H. Miranti, Sandeep Dasgupta, and Grigore Ro\u015fu. 2019. Formalizing x86-64 Instruction Decoder in K. In Workshop on Instruction Set Architecture Specification (co-located with ITP 2019)."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_53_1","unstructured":"M. O. Myreen M. J. C. Gordon and K. Slind. 2012. Decompilation into logic \u2014 Improved. In 2012 Formal Methods in Computer-Aided Design (FMCAD). 78\u201381. Scalable Validation of Binary Lifters PLDI \u201920 June 15\u201320 2020 London UK"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)81042-9"},{"key":"e_1_3_2_1_56_1","volume-title":"Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998)","author":"Pnueli Amir","year":"1998","unstructured":"Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation. In Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS \u201998). Springer-Verlag, Berlin, Heidelberg, 151\u2013166. http: \/\/dl.acm.org\/citation.cfm?id=646482.691453"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964002"},{"key":"e_1_3_2_1_58_1","unstructured":"Andrew Ruef and Artem Dinaburg. 2014. Static Translation of X86 Instruction Semantics to LLVM with McSema. https:\/\/github.com\/ trailofbits\/mcsema"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/BigData.Congress.2014.79"},{"key":"e_1_3_2_1_60_1","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi. 2011. Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA."},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the 22Nd USENIX Conference on Security (Washington, D.C.) (SEC\u201913)","author":"Schwartz Edward J.","year":"2013","unstructured":"Edward J. Schwartz, JongHyup Lee, Maverick Woo, and David Brumley. 2013. Native x86 Decompilation Using Semantics-preserving Structural Analysis and Iterative Control-flow Structuring. In Proceedings of the 22Nd USENIX Conference on Security (Washington, D.C.) (SEC\u201913). USENIX Association, Berkeley, CA, USA, 353\u2013368. http:\/\/dl.acm.org\/citation.cfm?id=2534766.2534797"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2012.6356589"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2380403.2380419"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"crossref","unstructured":"Yan Shoshitaishvili Ruoyu Wang Christopher Salls Nick Stephens Mario Polino Audrey Dutcher John Grosen Siji Feng Christophe Hauser Christopher Kruegel and Giovanni Vigna. 2016. SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis. (2016).","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_2_1_67_1","volume-title":"Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.)","author":"Slind Konrad","unstructured":"Konrad Slind and Michael Norrish. 2008. A Brief Overview of HOL4. In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, C\u00e9sar Mu\u00f1oz, and Sofi\u00e8ne Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 28\u201332."},{"key":"e_1_3_2_1_68_1","unstructured":"Aaron Smith and S. Bharadwaj Yadavalli. 2018. LLVM Based Binary Raiser: llvm-mctoll. (2018)."},{"key":"e_1_3_2_1_69_1","unstructured":"https:\/\/github.com\/Microsoft\/llvm-mctoll"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178260"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032364"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/358198.358210"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Khaled Yakdan Sebastian Eschweiler Elmar Gerhards-Padilla and Matthew Smith. 2015. No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations. In NDSS.","DOI":"10.14722\/ndss.2015.23185"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.25"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.44"},{"key":"e_1_3_2_1_78_1","volume-title":"Proceedings of the 22nd USENIX Conference on Security (Washington, D.C.) (SEC\u201913)","author":"Zhang Mingwei","unstructured":"Mingwei Zhang and R. Sekar. 2013. Control Flow Integrity for COTS Binaries. In Proceedings of the 22nd USENIX Conference on Security (Washington, D.C.) (SEC\u201913). USENIX Association, USA, 337\u2013352. Abstract 1 Introduction 2 Approach Overview 3 Preliminaries 4 Single-Instruction Translation Validation 5 Program-Level Validation 5.1 Compositional Lifter 5.2 Transformer & Matcher 6 Evaluation 7 Discussion 8 Related Work 8.1 Testing Based Approaches 8.2 Formal Methods Based Approaches 9 Conclusion Acknowledgments References"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385964","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3385964","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3385964","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:14Z","timestamp":1750200074000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3385964"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":76,"alternative-id":["10.1145\/3385412.3385964","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3385964","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}