{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T04:07:59Z","timestamp":1776398879408,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":67,"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.3523434","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"825-840","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Islaris: verification of machine code against authoritative ISA semantics"],"prefix":"10.1145","author":[{"given":"Michael","family":"Sammler","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Angus","family":"Hammond","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Rodolphe","family":"Lepigre","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The RISC-V Instruction Set Manual. Volume I: User-Level ISA","unstructured":"2017. The RISC-V Instruction Set Manual. Volume I: User-Level ISA ; Volume II : Privileged Architecture . https:\/\/riscv.org\/specifications\/ 2017. The RISC-V Instruction Set Manual. Volume I: User-Level ISA; Volume II: Privileged Architecture. https:\/\/riscv.org\/specifications\/"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12466-7_1"},{"key":"e_1_3_2_1_5_1","unstructured":"Arm. 2021. Arm Architecture Reference Manual. Armv8 for A-profile architecture profile. https:\/\/developer.arm.com\/documentation\/ddi0487\/ DDI 0487G.b. 8.7 EAC updated. 8696 pages.  Arm. 2021. Arm Architecture Reference Manual. Armv8 for A-profile architecture profile. https:\/\/developer.arm.com\/documentation\/ddi0487\/ DDI 0487G.b. 8.7 EAC updated. 8696 pages."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_2_1_8_1","unstructured":"Alasdair Armstrong Alastair Reid Thomas Bauereiss Peter Sewell Kathryn Gray and Anthony Fox. 2019. Sail ARMv8.5-A ISA model.  https:\/\/github.com\/rems-project\/sail-arm  Alasdair Armstrong Alastair Reid Thomas Bauereiss Peter Sewell Kathryn Gray and Anthony Fox. 2019. Sail ARMv8.5-A ISA model.  https:\/\/github.com\/rems-project\/sail-arm"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuCNC.2016.7561034"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886658"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314601"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_12"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018621"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_12"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48628-4_8"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987600"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160558"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908121"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_3"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_38_1","unstructured":"Xavier Leroy. 2017. CompCert 3.1. http:\/\/compcert.inria.fr\/  Xavier Leroy. 2017. CompCert 3.1. http:\/\/compcert.inria.fr\/"},{"key":"e_1_3_2_1_39_1","volume-title":"USENIX Security","author":"Li Shih-Wei","unstructured":"Shih-Wei Li , Xupeng Li , Ronghui Gu , Jason Nieh , and John Zhuang Hui . 2021. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor . In USENIX Security . USENIX Association , 3953\u20133970. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-shih-wei Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In USENIX Security. USENIX Association, 3953\u20133970. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-shih-wei"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_24"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79980-1_22"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_3_2_1_44_1","unstructured":"Prashanth Mundkur Jon French Brian Campbell Robert Norton-Wright Alasdair Armstrong Thomas Bauereiss Shaked Flur Christopher Pulte and Peter Sewell. 2014\u20132021. Sail RISC-V ISA model.  https:\/\/github.com\/riscv\/sail-riscv  Prashanth Mundkur Jon French Brian Campbell Robert Norton-Wright Alasdair Armstrong Thomas Bauereiss Shaked Flur Christopher Pulte and Peter Sewell. 2014\u20132021. Sail RISC-V ISA model.  https:\/\/github.com\/riscv\/sail-riscv"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_48_1","volume-title":"Decompilation into logic - Improved","author":"Myreen Magnus O.","unstructured":"Magnus O. Myreen , Michael J. C. Gordon , and Konrad Slind . 2012. Decompilation into logic - Improved . In FMCAD. IEEE , 78\u201381. https:\/\/ieeexplore.ieee.org\/document\/6462558\/ Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. 2012. Decompilation into logic - Improved. In FMCAD. IEEE, 78\u201381. https:\/\/ieeexplore.ieee.org\/document\/6462558\/"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_47"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498683"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077658"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_16"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6320641"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480929"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_32"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09539-7"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158097"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_3_2_1_66_1","unstructured":"The Bedrock Team. 2015. Verification of memcpy. https:\/\/github.com\/mit-plv\/bedrock\/blob\/e3ff3c2cba9976ac4351caaabb4bf\/Bedrock\/Examples\/Arr.v  The Bedrock Team. 2015. Verification of memcpy. https:\/\/github.com\/mit-plv\/bedrock\/blob\/e3ff3c2cba9976ac4351caaabb4bf\/Bedrock\/Examples\/Arr.v"},{"key":"e_1_3_2_1_67_1","unstructured":"The CompCert Team. 2021. CompCert Arm semantics. https:\/\/github.com\/AbsInt\/CompCert\/blob\/d194e47a7d494944385ff61c194693f8a67787cb\/aarch64\/Asm.v  The CompCert Team. 2021. CompCert Arm semantics. https:\/\/github.com\/AbsInt\/CompCert\/blob\/d194e47a7d494944385ff61c194693f8a67787cb\/aarch64\/Asm.v"},{"key":"e_1_3_2_1_68_1","unstructured":"The RISC-V Team. 2019. ISA Formal Spec Public Review. https:\/\/github.com\/riscvarchive\/ISA_Formal_Spec_Public_Review\/blob\/master\/comparison_table.md  The RISC-V Team. 2019. ISA Formal Spec Public Review. https:\/\/github.com\/riscvarchive\/ISA_Formal_Spec_Public_Review\/blob\/master\/comparison_table.md"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"}],"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.3523434","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523434","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:16Z","timestamp":1750188676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523434"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":67,"alternative-id":["10.1145\/3519939.3523434","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523434","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"}}]}}