{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:11:51Z","timestamp":1775873511634,"version":"3.50.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030587673","type":"print"},{"value":"9783030587680","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"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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-58768-0_14","type":"book-chapter","created":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:02:48Z","timestamp":1599825768000},"page":"247-264","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Sound C Code Decompilation for a Subset of x86-64 Binaries"],"prefix":"10.1007","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Olivier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Binoy","family":"Ravindran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,9,8]]},"reference":[{"key":"14_CR1","unstructured":"National Security Agency. Ghidra (2019). \nhttps:\/\/www.nsa.gov\/resources\/everyone\/ghidra\/"},{"key":"14_CR2","unstructured":"Andriesse, D., Chen, X., Van Der Veen, V., Slowinska, A., Bos, H.: An in-depth analysis of disassembly on full-scale x86\/x64 binaries. In: 25th USENIX Security Symposium (USENIX Security 2016), pp. 583\u2013600 (2016)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-540-31985-6_19","volume-title":"Compiler Construction","author":"G Balakrishnan","year":"2005","unstructured":"Balakrishnan, G., Gruian, R., Reps, T., Teitelbaum, T.: CodeSurfer\/x86\u2014a platform for analyzing x86 executables. In: Bodik, R. (ed.) CC 2005. LNCS, vol. 3443, pp. 250\u2013254. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31985-6_19"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bauman, E., Lin, Z., Hamlen, K.W.: Superset disassembly: statically rewriting x86 binaries without heuristics. In: NDSS (2018)","DOI":"10.14722\/ndss.2018.23300"},{"key":"14_CR5","unstructured":"Bellard, F.: QEMU, a fast and portable dynamic translator. In: USENIX Annual Technical Conference, FREENIX Track, vol. 41, p. 46 (2005)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bienia, C., Kumar, S., Singh, J.P., Li, K.: The PARSEC benchmark suite: characterization and architectural implications. In: Proceedings of the 17th International Conference on Parallel Architectures and Compilation Techniques, pp. 72\u201381. ACM (2008)","DOI":"10.1145\/1454115.1454128"},{"key":"14_CR7","unstructured":"Bonfante, G., Kaczmarek, M., Marion, J.-Y.: Control flow graphs as malware signatures (2007)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-22110-1_37","volume-title":"Computer Aided Verification","author":"D Brumley","year":"2011","unstructured":"Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: a binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 463\u2013469. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_37"},{"key":"14_CR9","unstructured":"Brumley, D., Lee, J.H., Schwartz, E.J., Woo, M.: Native x86 decompilation using semantics-preserving structural analysis and iterative control-flow structuring. In: Presented as part of the 22nd USENIX Security Symposium (USENIX Security 2013), pp. 353\u2013368 (2013)"},{"issue":"1","key":"14_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2200\/S00754ED1V01Y201701CAC038","volume":"12","author":"E Bugnion","year":"2017","unstructured":"Bugnion, E., Nieh, J., Tsafrir, D.: Hardware and software support for virtualization. Synth. Lect. Comput. Archit. 12(1), 1\u2013206 (2017)","journal-title":"Synth. Lect. Comput. Archit."},{"issue":"7","key":"14_CR11","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1002\/spe.4380250706","volume":"25","author":"C Cifuentes","year":"1995","unstructured":"Cifuentes, C., Gough, K.J.: Decompilation of binary programs. Softw. Pract. Exp. 25(7), 811\u2013829 (1995)","journal-title":"Softw. Pract. Exp."},{"key":"14_CR12","unstructured":"Cifuentes, C., Simon, D., Fraboulet, A.: Assembly to high-level language translation. In: Proceedings of International Conference on Software Maintenance (Cat. No. 98CB36272), pp. 228\u2013237. IEEE (1998)"},{"key":"14_CR13","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). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"14_CR14","unstructured":"Dinaburg, A., Ruef, A.: Mcsema: static translation of x86 instructions to LLVM. In: ReCon 2014 Conference, Montreal, Canada (2014)"},{"key":"14_CR15","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-23141-4_8","volume-title":"Information Security and Assurance","author":"L \u010eurfina","year":"2011","unstructured":"\u010eurfina, L., et al.: Design of a retargetable decompiler for a static platform-independent malware analysis. In: Kim, T., Adeli, H., Robles, R.J., Balitanas, M. (eds.) ISA 2011. CCIS, vol. 200, pp. 72\u201386. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-23141-4_8"},{"key":"14_CR16","unstructured":"Ferguson, J., Kaminsky, D.: Reverse engineering code with IDA Pro. Syngress (2008)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Fokin, A., Derevenetc, E., Chernov, A., Troshina, K.: SmartDec: approaching C++ decompilation. In: 2011 18th Working Conference on Reverse Engineering, pp. 347\u2013356. IEEE (2011)","DOI":"10.1109\/WCRE.2011.49"},{"issue":"1","key":"14_CR18","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"SM German","year":"1975","unstructured":"German, S.M., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Trans. Softw. Eng. 1(1), 68\u201375 (1975)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR19","unstructured":"Guilfanov, I.: Decompilers and beyond. Black Hat USA (2008)"},{"issue":"3","key":"14_CR20","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1145\/321832.321835","volume":"21","author":"MS Hecht","year":"1974","unstructured":"Hecht, M.S., Ullman, J.D.: Characterizations of reducible flow graphs. J. ACM (JACM) 21(3), 367\u2013375 (1974)","journal-title":"J. ACM (JACM)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Heule, S., Schkufza, E., Sharma, R., Aiken, A.: Stratified synthesis: automatically learning the x86-64 instruction set. In: ACM SIGPLAN Notices, vol. 51, pp. 237\u2013250. ACM (2016)","DOI":"10.1145\/2980983.2908121"},{"issue":"3","key":"14_CR22","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1093\/comjnl\/23.3.223","volume":"23","author":"RN Horspool","year":"1980","unstructured":"Horspool, R.N., Marovac, N.: An approach to the problem of detranslation of computer programs. Comput. J. 23(3), 223\u2013229 (1980)","journal-title":"Comput. J."},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Khadra, M.A.B., Stoffel, D., Kunz, W.: Speculative disassembly of binary code. In: 2016 International Conference on Compliers, Architectures, and Sythesis of Embedded Systems (CASES), pp. 1\u201310, October 2016","DOI":"10.1145\/2968455.2968505"},{"issue":"3","key":"14_CR24","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). \nhttps:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"14_CR25","unstructured":"K\u0159oustek, J.: Retargetable analysis of machine code. Ph.D. thesis, Brno, FIT BUT (2014)"},{"key":"14_CR26","unstructured":"K\u0159oustek, J., Kol\u00e1r, D.: Preprocessing of binary executable files towards retargetable decompilation. In: 8th International Multi-Conference on Computing in the Global Information Technology (ICCGI 2013), pp. 259\u2013264 (2013)"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Lankes, S., Pickartz, S., Breitbart, J.: Hermitcore: a unikernel for extreme scale computing. In: Proceedings of the 6th International Workshop on Runtime and Operating Systems for Supercomputers, p. 4. ACM (2016)","DOI":"10.1145\/2931088.2931093"},{"issue":"4","key":"14_CR28","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1145\/2499368.2451167","volume":"48","author":"A Madhavapeddy","year":"2013","unstructured":"Madhavapeddy, A., et al.: Unikernels: library operating systems for the cloud. ACM SIGPLAN Not. 48(4), 461\u2013472 (2013)","journal-title":"ACM SIGPLAN Not."},{"issue":"239","key":"14_CR29","first-page":"2","volume":"2014","author":"D Merkel","year":"2014","unstructured":"Merkel, D.: Docker: lightweight Linux containers for consistent development and deployment. Linux J. 2014(239), 2 (2014)","journal-title":"Linux J."},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"Mycroft, A.: Type-based decompilation (or program reconstruction via type reconstruction). In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 208\u2013223. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-49099-X_14","DOI":"10.1007\/3-540-49099-X_14"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, pp. 1\u20138, November 2008","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"14_CR32","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic - improved. In: 2012 Formal Methods in Computer-Aided Design (FMCAD), pp. 78\u201381. IEEE (2012)"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Olivier, P., Chiba, D., Lankes, S., Min, C., Ravindran, B.: A binary-compatible unikernel. In: Proceedings of the 15th ACM SIGPLAN\/SIGOPS International Conference on Virtual Execution Environments (VEE 2019) (2019)","DOI":"10.1145\/3313808.3313817"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Padioleau, Y., Lawall, J., Hansen, R.R., Muller, G.: Documenting and automating collateral evolutions in Linux device drivers. In: Proceedings of the 3rd ACM SIGOPS\/EuroSys European Conference on Computer Systems 2008, Eurosys 2008, pp. 247\u2013260. ACM, New York (2008)","DOI":"10.1145\/1352592.1352618"},{"key":"14_CR36","doi-asserted-by":"crossref","unstructured":"Padioleau, Y., Lawall, J.L., Muller, G.: Semantic patches, documenting and automating collateral evolutions in Linux device drivers. In: Ottawa Linux Symposium (OLS 2007), Ottawa, Canada (2007)","DOI":"10.1145\/1215995.1216005"},{"key":"14_CR37","unstructured":"Proebsting, T.A., Watterson, S.A.: Krakatoa: decompilation in Java (does bytecode reveal source?). In: COOTS, pp. 185\u2013198 (1997)"},{"key":"14_CR38","doi-asserted-by":"crossref","unstructured":"Roessle, I., Verbeek, F., Ravindran, B.: Formally verified big step semantics out of x86-64 binaries. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 181\u2013195. ACM (2019)","DOI":"10.1145\/3293880.3294102"},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Shoshitaishvili, Y., et al.: SoK: (state of) the art of war: offensive techniques in binary analysis. In: IEEE Symposium on Security and Privacy (2016)","DOI":"10.1109\/SP.2016.17"},{"key":"14_CR40","doi-asserted-by":"crossref","unstructured":"Sulaman, S.M., Orucevic-Alagic, A., Borg, M., Wnuk, K., H\u00f6st, M., de la Vara, J.L.: Development of safety-critical software systems using open source software - a systematic map. In: 2014 40th EUROMICRO Conference on Software Engineering and Advanced Applications (SEAA), pp. 17\u201324. IEEE (2014)","DOI":"10.1109\/SEAA.2014.25"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Wang, R., et al.: Ramblr: making reassembly great again. In: NDSS (2017)","DOI":"10.14722\/ndss.2017.23225"},{"key":"14_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-540-74061-2_11","volume-title":"Static Analysis","author":"T Wei","year":"2007","unstructured":"Wei, T., Mao, J., Zou, W., Chen, Y.: A new algorithm for identifying loops in decompilation. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 170\u2013183. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-74061-2_11"},{"key":"14_CR43","unstructured":"Liang, X., Sun, F., Zhendong, S.: Constructing precise control flow graphs from binaries. University of California, Davis, Technical report (2009)"},{"key":"14_CR44","doi-asserted-by":"crossref","unstructured":"Yakdan, K., Eschweiler, S., Gerhards-Padilla, E., Smith, M.: No more gotos: decompilation using pattern-independent control-flow structuring and semantic-preserving transformations. In: NDSS (2015)","DOI":"10.14722\/ndss.2015.23185"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-58768-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T12:04:58Z","timestamp":1599825898000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-58768-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030587673","9783030587680"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-58768-0_14","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":"8 September 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Amsterdam","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","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":"14 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/event.cwi.nl\/sefm2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}