{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,9]],"date-time":"2026-07-09T15:32:45Z","timestamp":1783611165013,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523702","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"934-949","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Formally verified lifting of C-compiled x86-64 binaries"],"prefix":"10.1145","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[{"name":"Open University of the Netherlands, Netherlands \/ Virginia Tech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joshua","family":"Bockenek","sequence":"additional","affiliation":[{"name":"Virginia Tech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhoulai","family":"Fu","sequence":"additional","affiliation":[{"name":"SUNY Korea, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[{"name":"Virginia Tech, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Avast Software. [n.d.]. RetDec :: Home. https:\/\/retdec.com\/ Accessed 2020-07-31.  Avast Software. [n.d.]. RetDec :: Home. https:\/\/retdec.com\/ Accessed 2020-07-31."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_19"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"e_1_3_2_1_4_1","volume-title":"23rd USENIX Security Symposium (USENIX Security 14)","author":"Bao Tiffany","year":"2014","unstructured":"Tiffany Bao , Jonathan Burket , Maverick Woo , Rafael Turner , and David Brumley . 2014 . BYTEWEIGHT: Learning to Recognize Functions in Binary Code . In 23rd USENIX Security Symposium (USENIX Security 14) . 845\u2013860. Tiffany Bao, Jonathan Burket, Maverick Woo, Rafael Turner, and David Brumley. 2014. BYTEWEIGHT: Learning to Recognize Functions in Binary Code. In 23rd USENIX Security Symposium (USENIX Security 14). 845\u2013860."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_13"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2968455.2968505"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_37"},{"key":"e_1_3_2_1_8_1","volume-title":"22nd USENIX Security Symposium (USENIX Security 13)","author":"Brumley David","year":"2013","unstructured":"David Brumley , JongHyup Lee , Edward J Schwartz , and Maverick Woo . 2013 . Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring . In 22nd USENIX Security Symposium (USENIX Security 13) . 353\u2013368. David Brumley, JongHyup Lee, Edward J Schwartz, and Maverick Woo. 2013. Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring. In 22nd USENIX Security Symposium (USENIX Security 13). 353\u2013368."},{"key":"e_1_3_2_1_9_1","unstructured":"David Chisnall. 2008. The Definitive Guide to the Xen Hypervisor. Pearson Education.  David Chisnall. 2008. The Definitive Guide to the Xen Hypervisor. Pearson Education."},{"key":"e_1_3_2_1_10_1","volume-title":"Introduction to algorithms","author":"Cormen Thomas H","unstructured":"Thomas H Cormen , Charles E Leiserson , Ronald L Rivest , and Clifford Stein . 2009. Introduction to algorithms . MIT press . Thomas H Cormen, Charles E Leiserson, Ronald L Rivest, and Clifford Stein. 2009. Introduction to algorithms. MIT press."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234740"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00074"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1655108.1655117"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.005"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_16_1","volume-title":"ReCon 2014 Conference","author":"Dinaburg Artem","year":"2014","unstructured":"Artem Dinaburg and Andrew Ruef . 2014 . McSema: Static translation of x86 instructions to LLVM . In ReCon 2014 Conference , Montreal, Canada. Artem Dinaburg and Andrew Ruef. 2014. McSema: Static translation of x86 instructions to LLVM. In ReCon 2014 Conference, Montreal, Canada."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385972"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2017.2785299"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2011.49"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_3_2_1_23_1","unstructured":"Hex-Rays SA. 2020. IDA Pro \u2013 Hex Rays. https:\/\/www.hex-rays.com\/products\/ida\/ Accessed 2020-07-06.  Hex-Rays SA. 2020. IDA Pro \u2013 Hex Rays. https:\/\/www.hex-rays.com\/products\/ida\/ Accessed 2020-07-06."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/23.3.223"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50995-8_3"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3134600.3134627"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2012.16"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_18"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-1539-9_11"},{"key":"e_1_3_2_1_33_1","volume-title":"Automating Mimicry Attacks Using Static Binary Analysis. In USENIX Security Symposium. 14","author":"Kruegel Christopher","year":"2005","unstructured":"Christopher Kruegel , Engin Kirda , Darren Mutz , William Robertson , and Giovanni Vigna . 2005 . Automating Mimicry Attacks Using Static Binary Analysis. In USENIX Security Symposium. 14 , 11\u201311. Christopher Kruegel, Engin Kirda, Darren Mutz, William Robertson, and Giovanni Vigna. 2005. Automating Mimicry Attacks Using Static Binary Analysis. In USENIX Security Symposium. 14, 11\u201311."},{"key":"e_1_3_2_1_34_1","volume-title":"Static Disassembly of Obfuscated Binaries. In USENIX Security Symposium. 13","author":"Kruegel Christopher","year":"2004","unstructured":"Christopher Kruegel , William Robertson , Fredrik Valeur , and Giovanni Vigna . 2004 . Static Disassembly of Obfuscated Binaries. In USENIX Security Symposium. 13 , 18\u201318. Christopher Kruegel, William Robertson, Fredrik Valeur, and Giovanni Vigna. 2004. Static Disassembly of Obfuscated Binaries. In USENIX Security Symposium. 13, 18\u201318."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_21"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00121"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_40_1","unstructured":"Magnus O. Myreen Michael J. C. Gordon and Konrad Slind. 2012. Decompilation into Logic \u2013 Improved. In 2012 Formal Methods in Computer-Aided Design (FMCAD). 78\u201381.  Magnus O. Myreen Michael J. C. Gordon and Konrad Slind. 2012. Decompilation into Logic \u2013 Improved. In 2012 Formal Methods in Computer-Aided Design (FMCAD). 78\u201381."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_43_1","unstructured":"NSA. 2019. Ghidra. https:\/\/ghidra-sre.org\/ Accessed 2020-07-06.  NSA. 2019. Ghidra. https:\/\/ghidra-sre.org\/ Accessed 2020-07-06."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22038-9_23"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.MEMICS.2010.101"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294102"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/358438.349325"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2002.1173063"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_51_1","volume-title":"ELF: A Spotlight on the Underappreciated Metadata. In 7th USENIX Workshop on Offensive Technologies (WOOT 13)","author":"Shapiro Rebecca","year":"2013","unstructured":"Rebecca Shapiro , Sergey Bratus , and Sean W Smith . 2013 . \u201c Weird Machines \u201d in ELF: A Spotlight on the Underappreciated Metadata. In 7th USENIX Workshop on Offensive Technologies (WOOT 13) . Rebecca Shapiro, Sergey Bratus, and Sean W Smith. 2013. \u201cWeird Machines\u201d in ELF: A Spotlight on the Underappreciated Metadata. In 7th USENIX Workshop on Offensive Technologies (WOOT 13)."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29613-5_12"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359986.3361215"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_6"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58768-0_14"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SecDev.2017.14"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2017.23225"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382216"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06608-0_23"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23808-6_34"},{"key":"e_1_3_2_1_62_1","unstructured":"Jordan Wiens. 2020. Binary Ninja. https:\/\/binary.ninja\/2020\/05\/11\/decompiler-stable-release.html Accessed 2020-07-06.  Jordan Wiens. 2020. Binary Ninja. https:\/\/binary.ninja\/2020\/05\/11\/decompiler-stable-release.html Accessed 2020-07-06."}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523702","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523702","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523702"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":60,"alternative-id":["10.1145\/3519939.3523702","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523702","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}