{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:52Z","timestamp":1776316852506,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["Sub HRL 17090-181687 US"],"award-info":[{"award-number":["Sub HRL 17090-181687 US"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1619275"],"award-info":[{"award-number":["1619275"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2996"],"award-info":[{"award-number":["N00014-17-1-2996"]}],"id":[{"id":"10.13039\/100007297","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314601","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"1133-1148","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["A complete formal semantics of x86-64 user-level instruction set architecture"],"prefix":"10.1145","author":[{"given":"Sandeep","family":"Dasgupta","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Daejun","family":"Park","sequence":"additional","affiliation":[{"name":"Runtime Verification, USA"}]},{"given":"Theodoros","family":"Kasampalis","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":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA \/ Runtime Verification, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2008. IEEE Std 754-2008 - IEEE Standard for Floating-Point Arithmetic. https:\/\/standards.ieee.org\/findstds\/standard\/754-2008.html.  2008. IEEE Std 754-2008 - IEEE Standard for Floating-Point Arithmetic. https:\/\/standards.ieee.org\/findstds\/standard\/754-2008.html."},{"key":"e_1_3_2_2_2_1","volume-title":"Sail x86 ISA model. https:\/\/github.com\/rems-project\/sail\/tree\/sail2\/x86. Last accessed","year":"2019","unstructured":"2017. Sail x86 ISA model. https:\/\/github.com\/rems-project\/sail\/tree\/sail2\/x86. Last accessed : May 2, 2019 . 2017. Sail x86 ISA model. https:\/\/github.com\/rems-project\/sail\/tree\/sail2\/x86. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_3_1","volume-title":"Angr: A powerful and user-friendly binary analysis platform! http:\/\/angr.io\/. Last accessed","year":"2019","unstructured":"2018. Angr: A powerful and user-friendly binary analysis platform! http:\/\/angr.io\/. Last accessed : May 2, 2019 . 2018. Angr: A powerful and user-friendly binary analysis platform! http:\/\/angr.io\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_4_1","volume-title":"Bug Reported in Intel Developer Zone: Possible errors in instruction semantics. https:\/\/software.intel.com\/en-us\/forums\/intel-isa-extensions\/topic\/773342. Last accessed","year":"2019","unstructured":"2018. Bug Reported in Intel Developer Zone: Possible errors in instruction semantics. https:\/\/software.intel.com\/en-us\/forums\/intel-isa-extensions\/topic\/773342. Last accessed : May 2, 2019 . 2018. Bug Reported in Intel Developer Zone: Possible errors in instruction semantics. https:\/\/software.intel.com\/en-us\/forums\/intel-isa-extensions\/topic\/773342. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_5_1","volume-title":"Bug Reported in Stoke: Modelling the behavior of flags which may or must take undef values. https:\/\/github.com\/StanfordPL\/stoke\/issues\/986. Last accessed","year":"2019","unstructured":"2018. Bug Reported in Stoke: Modelling the behavior of flags which may or must take undef values. https:\/\/github.com\/StanfordPL\/stoke\/issues\/986. Last accessed : May 2, 2019 . 2018. Bug Reported in Stoke: Modelling the behavior of flags which may or must take undef values. https:\/\/github.com\/StanfordPL\/stoke\/issues\/986. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_6_1","volume-title":"Bug Reported in Stoke: Semantic bugs. https:\/\/github.com\/StanfordPL\/stoke\/issues\/983. Last accessed","year":"2019","unstructured":"2018. Bug Reported in Stoke: Semantic bugs. https:\/\/github.com\/StanfordPL\/stoke\/issues\/983. Last accessed : May 2, 2019 . 2018. Bug Reported in Stoke: Semantic bugs. https:\/\/github.com\/StanfordPL\/stoke\/issues\/983. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_7_1","volume-title":"C Language Testsuites: C-torture version 8.1.0. https:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html. Last accessed","year":"2019","unstructured":"2018. C Language Testsuites: C-torture version 8.1.0. https:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html. Last accessed : May 2, 2019 . 2018. C Language Testsuites: C-torture version 8.1.0. https:\/\/gcc.gnu.org\/onlinedocs\/gccint\/C-Tests.html. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_8_1","unstructured":"2018. Eric Schkufza. Personal communication.  2018. Eric Schkufza. Personal communication."},{"key":"e_1_3_2_2_9_1","volume-title":"Evaluable Strings Intermediate Language. https:\/\/radare.gitbooks.io\/radare2book\/content\/disassembling\/esil.html. Last accessed","year":"2019","unstructured":"2018. Evaluable Strings Intermediate Language. https:\/\/radare.gitbooks.io\/radare2book\/content\/disassembling\/esil.html. Last accessed : May 2, 2019 . 2018. Evaluable Strings Intermediate Language. https:\/\/radare.gitbooks.io\/radare2book\/content\/disassembling\/esil.html. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_10_1","volume-title":"GDB: The GNU Project Debugger. https:\/\/www.gnu.org\/software\/gdb\/. Last accessed","year":"2019","unstructured":"2018. GDB: The GNU Project Debugger. https:\/\/www.gnu.org\/software\/gdb\/. Last accessed : May 2, 2019 . 2018. GDB: The GNU Project Debugger. https:\/\/www.gnu.org\/software\/gdb\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_11_1","volume-title":"Published on","year":"2016","unstructured":"2018. Intel 64 and IA-32 Architectures Software Developer Manuals. https:\/\/software.intel.com\/en-us\/articles\/intel-sdm . Published on October 12, 2016 , updated May 18, 2018. 2018. Intel 64 and IA-32 Architectures Software Developer Manuals. https:\/\/software.intel.com\/en-us\/articles\/intel-sdm. Published on October 12, 2016, updated May 18, 2018."},{"key":"e_1_3_2_2_12_1","volume-title":"MPFR Java Bindings. https:\/\/github.com\/kframework\/mpfr-java. Last accessed","year":"2019","unstructured":"2018. MPFR Java Bindings. https:\/\/github.com\/kframework\/mpfr-java. Last accessed : May 2, 2019 . 2018. MPFR Java Bindings. https:\/\/github.com\/kframework\/mpfr-java. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_13_1","volume-title":"Remill: Library for lifting of x86, amd64, and aarch64 machine code to LLVM bitcode. https:\/\/github.com\/trailofbits\/remill. Last accessed","year":"2019","unstructured":"2018. Remill: Library for lifting of x86, amd64, and aarch64 machine code to LLVM bitcode. https:\/\/github.com\/trailofbits\/remill. Last accessed : May 2, 2019 . 2018. Remill: Library for lifting of x86, amd64, and aarch64 machine code to LLVM bitcode. https:\/\/github.com\/trailofbits\/remill. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_14_1","volume-title":"The Coq Proof Assistant. https:\/\/coq.inria.fr\/. Last accessed","year":"2019","unstructured":"2018. The Coq Proof Assistant. https:\/\/coq.inria.fr\/. Last accessed : May 2, 2019 . 2018. The Coq Proof Assistant. https:\/\/coq.inria.fr\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_15_1","volume-title":"The GNU MPFR Library. https:\/\/www.mpfr.org\/. Last accessed","year":"2019","unstructured":"2018. The GNU MPFR Library. https:\/\/www.mpfr.org\/. Last accessed : May 2, 2019 . 2018. The GNU MPFR Library. https:\/\/www.mpfr.org\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_16_1","unstructured":"2018. x86 and amd64 Instruction Reference (UnOfficial). http:\/\/www.felixcloutier.com\/x86\/. Last accessed: May 2 2019.  2018. x86 and amd64 Instruction Reference (UnOfficial). http:\/\/www.felixcloutier.com\/x86\/. Last accessed: May 2 2019."},{"key":"e_1_3_2_2_17_1","unstructured":"2018. X86isa: Implemented-opcodes: Opcodes supported by the x86 model. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/index-seo.php\/X86ISA____IMPLEMENTED-OPCODES. Last accessed: May 2 2019.  2018. X86isa: Implemented-opcodes: Opcodes supported by the x86 model. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/manual\/index-seo.php\/X86ISA____IMPLEMENTED-OPCODES. Last accessed: May 2 2019."},{"key":"e_1_3_2_2_18_1","volume-title":"RISC-V, Power, and x86. https:\/\/github.com\/rems-project\/rmem\/. Last accessed","year":"2019","unstructured":"2019. rmem: Executable concurrency models for ARMv8 , RISC-V, Power, and x86. https:\/\/github.com\/rems-project\/rmem\/. Last accessed : May 2, 2019 . 2019. rmem: Executable concurrency models for ARMv8, RISC-V, Power, and x86. https:\/\/github.com\/rems-project\/rmem\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_19_1","volume-title":"Automation Test in Europe Conference Exhibition (DATE). 1538s1543","author":"Ahmed A.","unstructured":"A. Ahmed , F. Farahmandi , and P. Mishra . 2018. Directed test generation using concolic testing on RTL models. In 2018 Design , Automation Test in Europe Conference Exhibition (DATE). 1538s1543 . A. Ahmed, F. Farahmandi, and P. Mishra. 2018. Directed test generation using concolic testing on RTL models. In 2018 Design, Automation Test in Europe Conference Exhibition (DATE). 1538s1543."},{"key":"e_1_3_2_2_20_1","volume-title":"https:\/\/rada.re\/r\/. Last accessed","author":"Alvarez Sergi","year":"2019","unstructured":"Sergi Alvarez . 2018. Radare2. https:\/\/rada.re\/r\/. Last accessed : May 2, 2019 . Sergi Alvarez. 2018. Radare2. https:\/\/rada.re\/r\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749612"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1247360.1247401"},{"key":"e_1_3_2_2_24_1","first-page":"463","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11)","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 (CAV'11) . Springer-Verlag, Berlin, Heidelberg , 463 - 469 . http:\/\/dl.acm.org\/citation.cfm?id= 2032 305.2032342. 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 (CAV'11). Springer-Verlag, Berlin, Heidelberg, 463-469. http:\/\/dl.acm.org\/citation.cfm?id=2032305.2032342."},{"key":"e_1_3_2_2_25_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08) . USENIX Association, Berkeley, CA, USA , 209 - 224 . http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855756. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08). USENIX Association, Berkeley, CA, USA, 209-224. http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855756."},{"key":"e_1_3_2_2_26_1","volume-title":"Semantics of x86-64 in K. https:\/\/github.com\/kframework\/X86-64-semantics. Last accessed","author":"Dasgupta Sandeep","year":"2019","unstructured":"Sandeep Dasgupta . 2018. Semantics of x86-64 in K. https:\/\/github.com\/kframework\/X86-64-semantics. Last accessed : May 2, 2019 . Sandeep Dasgupta. 2018. Semantics of x86-64 in K. https:\/\/github.com\/kframework\/X86-64-semantics. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_27_1","volume-title":"Defining semantics of instructions unsupported in Strata\/Stoke. https:\/\/github.com\/StanfordPL\/stoke\/pull\/996. Last accessed","author":"Dasgupta Sandeep","year":"2019","unstructured":"Sandeep Dasgupta . 2019. Defining semantics of instructions unsupported in Strata\/Stoke. https:\/\/github.com\/StanfordPL\/stoke\/pull\/996. Last accessed : May 2, 2019 . Sandeep Dasgupta. 2019. Defining semantics of instructions unsupported in Strata\/Stoke. https:\/\/github.com\/StanfordPL\/stoke\/pull\/996. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_28_1","volume-title":"Improving Stoke ability to debug a circuit. https:\/\/github.com\/StanfordPL\/stoke\/pull\/997. Last accessed","author":"Dasgupta Sandeep","year":"2019","unstructured":"Sandeep Dasgupta . 2019. Improving Stoke ability to debug a circuit. https:\/\/github.com\/StanfordPL\/stoke\/pull\/997. Last accessed : May 2, 2019 . Sandeep Dasgupta. 2019. Improving Stoke ability to debug a circuit. https:\/\/github.com\/StanfordPL\/stoke\/pull\/997. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2744769.2744921"},{"key":"e_1_3_2_2_32_1","volume-title":"Executable x86 ISA Simulator for Software Verification","author":"Goel Shilpi","unstructured":"Shilpi Goel , Warren A. Hunt , and Matt Kaufmann . 2017. Engineering a Formal , Executable x86 ISA Simulator for Software Verification . Springer International Publishing , Cham , 173-209. Shilpi Goel, Warren A. Hunt, and Matt Kaufmann. 2017. Engineering a Formal, Executable x86 ISA Simulator for Software Verification. Springer International Publishing, Cham, 173-209."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682944"},{"key":"e_1_3_2_2_34_1","first-page":"653","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI'16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI'16) . USENIX Association, Berkeley, CA, USA , 653 - 669 . http:\/\/dl.acm.org\/citation.cfm?id=3026877.3026928. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI'16). USENIX Association, Berkeley, CA, USA, 653-669. http:\/\/dl.acm.org\/citation.cfm?id=3026877.3026928."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950335"},{"key":"e_1_3_2_2_36_1","first-page":"311","volume-title":"Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '16)","author":"Hasabnis Niranjan","unstructured":"Niranjan Hasabnis and R. Sekar . 2016. Lifting Assembly to Intermediate Representation: A Novel Approach Leveraging Compilers . In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '16) . ACM, New York, NY, USA , 311 - 324 . Niranjan Hasabnis and R. Sekar. 2016. Lifting Assembly to Intermediate Representation: A Novel Approach Leveraging Compilers. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '16). ACM, New York, NY, USA, 311-324."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_3_2_2_38_1","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann Matt","unstructured":"Matt Kaufmann , J. Strother Moore , and Panagiotis Manolios . 2000. Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , Norwell, MA, USA . Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell, MA, USA."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_2_40_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 . 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_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_3_2_2_43_1","first-page":"1","article-title":"Efficient validation input generation in RTL by hybridized source code analysis. In 2011 Design","author":"Liu L.","year":"2011","unstructured":"L. Liu and S. Vasudevan . 2011 . Efficient validation input generation in RTL by hybridized source code analysis. In 2011 Design , Automation Test in Europe. 1 - 6 . L. Liu and S. Vasudevan. 2011. Efficient validation input generation in RTL by hybridized source code analysis. In 2011 Design, Automation Test in Europe. 1-6.","journal-title":"Automation Test in Europe."},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676549"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2151012"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)81042-9"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3264591"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_2_51_1","volume-title":"ARM's Architecture Specification Language. https:\/\/alastairreid.github.io\/specification_languages\/. Last accessed","author":"Reid Alastair","year":"2019","unstructured":"Alastair Reid . 2016. ARM's Architecture Specification Language. https:\/\/alastairreid.github.io\/specification_languages\/. Last accessed : May 2, 2019 . Alastair Reid. 2016. ARM's Architecture Specification Language. https:\/\/alastairreid.github.io\/specification_languages\/. Last accessed: May 2, 2019."},{"key":"e_1_3_2_2_52_1","first-page":"161","volume-title":"Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016","author":"Reid Alastair","year":"2017","unstructured":"Alastair Reid . 2017 . Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture . Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016 (2017), 161 - 168 . Alastair Reid. 2017. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016 (2017), 161-168."},{"key":"e_1_3_2_2_53_1","first-page":"555","volume-title":"Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA' 12)","author":"Ro\u00feu Grigore","year":"2012","unstructured":"Grigore Ro\u00feu and Andrei \u00detef?nescu. 2012 . Checking Reachability using Matching Logic . In Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA' 12) . ACM, 555 - 574 . https:\/\/doi.org\/citation.cfm?doid=2384616.2384656. Grigore Ro\u00feu and Andrei \u00detef?nescu. 2012. Checking Reachability using Matching Logic. In Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA' 12). ACM, 555-574. https:\/\/doi.org\/citation.cfm?doid=2384616.2384656."},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294102"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_2_2_56_1","volume-title":"Static Translation of X86 Instruction Semantics to LLVM with McSema. REcon","author":"Ruef Andrew","year":"2014","unstructured":"Andrew Ruef and Artem Dinaburg . 2014. Static Translation of X86 Instruction Semantics to LLVM with McSema. REcon ( 2014 ). https:\/\/github.com\/trailofbits\/mcsema. Andrew Ruef and Artem Dinaburg. 2014. Static Translation of X86 Instruction Semantics to LLVM with McSema. REcon (2014). https:\/\/github.com\/trailofbits\/mcsema."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_2_58_1","first-page":"305","volume-title":"Stochastic Superoptimization. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '13)","author":"Schkufza Eric","year":"2013","unstructured":"Eric Schkufza , Rahul Sharma , and Alex Aiken . 2013 . Stochastic Superoptimization. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '13) . ACM, New York, NY, USA , 305 - 316 . Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic Superoptimization. In Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '13). ACM, New York, NY, USA, 305-316."},{"key":"e_1_3_2_2_60_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).  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_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737960"},{"key":"e_1_3_2_2_62_1","first-page":"74","volume-title":"Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA","author":"Andrei","year":"2016","unstructured":"Andrei Stef?nescu, Daejun Park , Shijiao Yuwen , Yilong Li , and Grigore Ro\u00feu . 2016 . Semantics-based Program Verifiers for All Languages . In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). ACM, New York, NY, USA , 74 - 91 . Andrei Stef?nescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Ro\u00feu. 2016. Semantics-based Program Verifiers for All Languages. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). ACM, New York, NY, USA, 74-91."},{"key":"e_1_3_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/358198.358210"},{"key":"e_1_3_2_2_64_1","first-page":"19","volume-title":"Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation -","volume":"7","author":"Zeldovich Nickolai","year":"2006","unstructured":"Nickolai Zeldovich , Silas Boyd-Wickizer , Eddie Kohler , and David Mazi\u00e8res . 2006 . Making Information Flow Explicit in HiStar . In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7 (OSDI '06). USENIX Association, Berkeley, CA, USA , 19 - 19 . http:\/\/dl.acm.org\/citation.cfm?id=1267308.1267327. Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazi\u00e8res. 2006. Making Information Flow Explicit in HiStar. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7 (OSDI '06). USENIX Association, Berkeley, CA, USA, 19-19. http:\/\/dl.acm.org\/citation.cfm?id=1267308.1267327."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314601","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314601","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314601","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":63,"alternative-id":["10.1145\/3314221.3314601","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314601","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}