{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:51Z","timestamp":1776305271128,"version":"3.50.1"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031747755","type":"print"},{"value":"9783031747762","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-74776-2_4","type":"book-chapter","created":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:35:33Z","timestamp":1737351333000},"page":"86-119","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Lift-Offline: Instruction Lifter Generators"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8758-0666","authenticated-orcid":false,"given":"Nicholas","family":"Coughlin","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7316-9112","authenticated-orcid":false,"given":"A.","family":"Michael","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2599-2259","authenticated-orcid":false,"given":"Kait","family":"Lam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,1,21]]},"reference":[{"key":"4_CR1","unstructured":"ARM: ARM Architecture Reference Manual for A-profile architecture (2023)"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Armstrong, A., et al.: ISA semantics for ARMv8-a, RISC-V, and CHERI-MIPS. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290384","DOI":"10.1145\/3290384"},{"key":"4_CR3","unstructured":"Avast Software: avast\/retdec: RetDec is a retargetable machine-code decompiler based on LLVM (2022). https:\/\/github.com\/avast\/retdec"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Balakrishnan, G., Reps, T.W.: WYSINWYX: what you see is not what you eXecute. ACM Trans. Program. Lang. Syst. 32(6), 23:1\u201323:84 (2010). https:\/\/doi.org\/10.1145\/1749608.1749612","DOI":"10.1145\/1749608.1749612"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Blazy, S., Hutin, R., Pichardie, D.: Secure compilation of constant-resource programs. In: 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, 21\u201325 June 2021, pp. 1\u201312. IEEE (2021). https:\/\/doi.org\/10.1109\/CSF51468.2021.00020","DOI":"10.1109\/CSF51468.2021.00020"},{"key":"4_CR6","unstructured":"Bellard, F.: QEMU, a fast and portable dynamic translator. In: Proceedings of the FREENIX Track: 2005 USENIX Annual Technical Conference, 10\u201315 April 2005, Anaheim, CA, USA, pp. 41\u201346. USENIX (2005). http:\/\/www.usenix.org\/events\/usenix05\/tech\/freenix\/bellard.html"},{"key":"4_CR7","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.) Computer Aided Verification, pp. 463\u2013469. Springer, Heidelberg (2011)"},{"issue":"8","key":"4_CR8","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986). https:\/\/doi.org\/10.1109\/TC.1986.1676819","journal-title":"IEEE Trans. Comput."},{"issue":"1","key":"4_CR9","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/963778.963784","volume":"26","author":"NH Christensen","year":"2004","unstructured":"Christensen, N.H., Gl\u00fcck, R.: Offline partial evaluation can be as accurate as online partial evaluation. ACM Trans. Program. Lang. Syst. 26(1), 191\u2013220 (2004). https:\/\/doi.org\/10.1145\/963778.963784","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Coughlin, N., Michael, A., Lam, K.: Artifact for \u201cLift-offline: instruction lifter generators\u201d (2024). https:\/\/doi.org\/10.5281\/zenodo.13219113","DOI":"10.5281\/zenodo.13219113"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Dasgupta, S., Park, D., Kasampalis, T., Adve, V.S., Ro\u015fu, G.: A complete formal semantics of x86-64 user-level instruction set architecture. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp. 1133\u20131148. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314601","DOI":"10.1145\/3314221.3314601"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"102725","DOI":"10.1016\/j.scico.2021.102725","volume":"213","author":"AS Dimovski","year":"2022","unstructured":"Dimovski, A.S., Apel, S., Legay, A.: Several lifted abstract domains for static analysis of numerical program families. Sci. Comput. Program. 213, 102725 (2022). https:\/\/doi.org\/10.1016\/j.scico.2021.102725","journal-title":"Sci. Comput. Program."},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"D\u2019Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, 21\u201322 May 2015, pp. 73\u201387. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/SPW.2015.33","DOI":"10.1109\/SPW.2015.33"},{"key":"4_CR14","unstructured":"Flores-Montoya, A., Schulte, E.M.: Datalog disassembly. In: Capkun, S., Roesner, F. (eds.) 29th USENIX Security Symposium, USENIX Security 2020, 12\u201314 August 2020, pp. 1075\u20131092. USENIX Association (2020). https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/flores-montoya"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25\u201340. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/10930755_2"},{"issue":"2\/3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst. Des. 10(2\/3), 149\u2013169 (1997). https:\/\/doi.org\/10.1023\/A:1008647823331","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Heule, S., Schkufza, E., Sharma, R., Aiken, A.: Stratified synthesis: automatically learning the x86-64 instruction set. In: Krintz, C., Berger, E.D. (eds.) Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13\u201317 June 2016, pp. 237\u2013250. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908121","DOI":"10.1145\/2908080.2908121"},{"key":"4_CR18","unstructured":"Intel Corporation: Intel A64 and IA-32 Architectures Software Developer\u2019s manual (2023)"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Jancar, J., et al.: They\u2019re not that hard to mitigate: what cryptographic library developers think about timing attacks. In: Rabiser, R., Wimmer, M., Groher, I., Wortmann, A., Wiesmayr, B. (eds.) Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, 26 February\u20131 March 2024. LNI, vol. P-343, pp. 143\u2013144. Gesellschaft f\u00fcr Informatik e.V. (2024). https:\/\/doi.org\/10.18420\/sw2024_47","DOI":"10.18420\/sw2024_47"},{"key":"4_CR20","unstructured":"Jeannet, B.: Bddapron (2012)"},{"key":"4_CR21","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall International Series in Computer Science. Prentice Hall (1993)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Kim, S., et al.: Testing intermediate representations for binary analysis. In: Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, pp. 353\u2013364. IEEE Press (2017)","DOI":"10.1109\/ASE.2017.8115648"},{"issue":"7","key":"4_CR23","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). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 179\u2013192. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Lam, K., Coughlin, N.: Lift-off: trustworthy ARMv8 semantics from formal specifications. In: Nadel, A., Rozier, K.Y. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, 24\u201327 October 2023, pp. 274\u2013283. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_36","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_36"},{"key":"4_CR26","unstructured":"Leino, K.R.M.: This is Boogie 2. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"issue":"4","key":"4_CR27","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason."},{"key":"4_CR28","unstructured":"Lhotak, O.: Program analysis using binary decision diagrams. Ph.D. thesis, School of Computer Science, McGill University, Montreal (2006)"},{"key":"4_CR29","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.scico.2019.01.001","volume":"174","author":"A Lindner","year":"2019","unstructured":"Lindner, A., Guanciale, R., Metere, R.: TrABin: trustworthy analyses of binaries. Sci. Comput. Program. 174, 72\u201389 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.01.001","journal-title":"Sci. Comput. Program."},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., Lee, J., Hur, C., Liu, Z., Regehr, J.: Alive2: bounded translation validation for LLVM. In: Freund, S.N., Yahav, E. (eds.) PLDI 2021: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, 20\u201325 June 2021, pp. 65\u201379. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"4_CR31","unstructured":"Mattsen, S.: BDD-based value analysis for X86 executables. Ph.D. thesis, Technical University of Hamburg, Germany (2017). http:\/\/tubdok.tub.tuhh.de\/handle\/11420\/1510"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Meng, X., Miller, B.P.: Binary code is not easy. In: Zeller, A., Roychoudhury, A. (eds.) Proceedings of the 25th International Symposium on Software Testing and Analysis, ISSTA 2016, Saarbr\u00fccken, Germany, 18\u201320 July 2016, pp. 24\u201335. ACM (2016). https:\/\/doi.org\/10.1145\/2931037.2931047","DOI":"10.1145\/2931037.2931047"},{"key":"4_CR33","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic - improved. In: Cabodi, G., Singh, S. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, 22\u201325 October 2012, pp. 78\u201381. IEEE (2012). https:\/\/ieeexplore.ieee.org\/document\/6462558\/"},{"key":"4_CR34","unstructured":"National Security Agency: Sleigh (2022). https:\/\/github.com\/NationalSecurityAgency\/ghidra"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-031-25803-9_7","volume-title":"Verified Software. Theories, Tools and Experiments","author":"N Naus","year":"2022","unstructured":"Naus, N., Verbeek, F., Walker, D., Ravindran, B.: A formal semantics for P-code. In: Lal, A., Tonetta, S. (eds.) VSTTE 2022. LNCS, vol. 13800, pp. 111\u2013128. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-25803-9_7"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Palsberg, J., Schwartzbach, M.I.: Binding-time analysis: abstract interpretation versus type inference. In: Bal, H.E. (ed.) Proceedings of the IEEE Computer Society 1994 International Conference on Computer Languages, 16\u201319 May 1994, Toulouse, France, pp. 277\u2013288. IEEE Computer Society (1994). https:\/\/doi.org\/10.1109\/ICCL.1994.288372","DOI":"10.1109\/ICCL.1994.288372"},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151\u2013166. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054170"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Reid, A.: Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In: Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016, pp. 161\u2013168, FMCAD Inc., Austin (2016)","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Reid, A.: Who guards the guards? Formal validation of the Arm v8-M architecture specification. Proc. ACM Program. Lang. 1(OOPSLA), 88:1\u201388:24 (2017). https:\/\/doi.org\/10.1145\/3133912","DOI":"10.1145\/3133912"},{"key":"4_CR40","unstructured":"Reid, A.: Using ASLi with arm\u2019s V8.6-A ISA specification (2020). https:\/\/alastairreid.github.io\/using-asli\/"},{"key":"4_CR41","doi-asserted-by":"publisher","unstructured":"Sammler, M., et al.: Islaris: verification of machine code against authoritative ISA semantics. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, pp. 825\u2013840. Association for Computing Machinery, New York (2022). https:\/\/doi.org\/10.1145\/3519939.3523434","DOI":"10.1145\/3519939.3523434"},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Sumii, E., Kobayashi, N.: Online-and-offline partial evaluation: a mixed approach (extended abstract). In: Lawall, J.L. (ed.) Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2000), Boston, Massachusetts, USA, 22\u201323 January 2000, pp. 12\u201321. ACM (2000). https:\/\/doi.org\/10.1145\/328690.328694","DOI":"10.1145\/328690.328694"},{"key":"4_CR43","unstructured":"Trail of Bits: lifting-bits\/remill: Library for lifting machine code to LLVM bitcode (2022). https:\/\/github.com\/lifting-bits\/remill"},{"key":"4_CR44","unstructured":"UQ-PAC: UQ-PAC\/BASIL (2024). https:\/\/github.com\/UQ-PAC\/BASIL"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-030-58768-0_14","volume-title":"Software Engineering and Formal Methods","author":"F Verbeek","year":"2020","unstructured":"Verbeek, F., Olivier, P., Ravindran, B.: Sound C code decompilation for a subset of x86-64 binaries. In: de Boer, F., Cerone, A. (eds.) SEFM 2020. LNCS, vol. 12310, pp. 247\u2013264. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58768-0_14"},{"key":"4_CR46","doi-asserted-by":"publisher","unstructured":"Wang, F., Shoshitaishvili, Y.: Angr - the next generation of binary analysis. In: IEEE Cybersecurity Development, SecDev 2017, Cambridge, MA, USA, 24\u201326 September 2017, pp. 8\u20139. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/SecDev.2017.14","DOI":"10.1109\/SecDev.2017.14"},{"key":"4_CR47","doi-asserted-by":"crossref","unstructured":"Winter, K., Coughlin, N., Smith, G.: Backwards-directed information flow analysis for concurrent programs. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pp. 1\u201316. IEEE (2021)","DOI":"10.1109\/CSF51468.2021.00017"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74776-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T05:35:41Z","timestamp":1737351341000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74776-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031747755","9783031747762"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74776-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2024.splashcon.org\/home\/sas-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}