{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T15:31:00Z","timestamp":1773588660184,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":87,"publisher":"ACM","license":[{"start":{"date-parts":[[2027,3,22]],"date-time":"2027-03-22T00:00:00Z","timestamp":1805673600000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Science Foundation","award":["CCF-2239484"],"award-info":[{"award-number":["CCF-2239484"]}]},{"name":"National Science Foundation","award":["CCF-2124080"],"award-info":[{"award-number":["CCF-2124080"]}]},{"name":"National Science Foundation","award":["CNS-2052947"],"award-info":[{"award-number":["CNS-2052947"]}]},{"name":"National Science Foundation","award":["CNS-2247370"],"award-info":[{"award-number":["CNS-2247370"]}]},{"name":"DARPA","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}]},{"name":"Amazon","award":["Amazon Research Award"],"award-info":[{"award-number":["Amazon Research Award"]}]},{"name":"VMware","award":["VMware Systems Research Award"],"award-info":[{"award-number":["VMware Systems Research Award"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,3,22]]},"DOI":"10.1145\/3779212.3790171","type":"proceedings-article","created":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T13:55:26Z","timestamp":1773150926000},"page":"912-928","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Highly Automated Verification of Security Properties for Unmodified System Software"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5703-2582","authenticated-orcid":false,"given":"Ganxiang","family":"Yang","sequence":"first","affiliation":[{"name":"Columbia University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2107-1625","authenticated-orcid":false,"given":"Wei","family":"Qiang","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2740-2109","authenticated-orcid":false,"given":"Yi","family":"Rong","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1371-2179","authenticated-orcid":false,"given":"Xuheng","family":"Li","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3378-006X","authenticated-orcid":false,"given":"Fanqi","family":"Yu","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8301-4479","authenticated-orcid":false,"given":"Jason","family":"Nieh","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6812-6182","authenticated-orcid":false,"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY, USA and CertiK, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,3,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987212"},{"key":"e_1_3_2_1_2_1","volume-title":"ARM Security Technology: Building a Secure System using TrustZone Technology. https:\/\/documentation-service.arm.com\/static\/5f212796500e883ab8e74531. Accessed","author":"Ltd ARM","year":"2025","unstructured":"ARM Ltd., 2009. ARM Security Technology: Building a Secure System using TrustZone Technology. https:\/\/documentation-service.arm.com\/static\/5f212796500e883ab8e74531. Accessed 22 Dec. 2025."},{"key":"e_1_3_2_1_3_1","volume-title":"https:\/\/www.trustedfirmware.org\/projects\/tf-rmm\/. Accessed","author":"Ltd ARM","year":"2025","unstructured":"ARM Ltd., 2023. TF-RMM. https:\/\/www.trustedfirmware.org\/projects\/tf-rmm\/. Accessed 22 Dec. 2025."},{"key":"e_1_3_2_1_4_1","unstructured":"D Elliot Bell and Leonard J LaPadula. 1973. Secure Computer Systems: Mathematical Foundations. Technical Report MTR-2547-VOL-1. MITRE Corp."},{"key":"e_1_3_2_1_5_1","unstructured":"Kenneth J Biba. 1977. Integrity Considerations for Secure Computer Systems. Technical Report MTR-3153-REV-1. MITRE Corp."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2200\/S00754ED1V01Y201701CAC038"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation","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 Symposium on Operating Systems Design and Implementation (San Diego, CA USA) (OSDI '08). 209\u2013224."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695980"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579854"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1987.10001"},{"key":"e_1_3_2_1_13_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"2000","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 2000. Model Checking. MIT Press."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_3_2_1_15_1","unstructured":"Victor Costan and Srinivas Devadas. 2016. Intel SGX Explained. Cryptology ePrint Archive Paper 2016\/086. https:\/\/eprint.iacr.org\/2016\/086"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640398"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3273982.3273987"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2016.35"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 2017 USENIX Annual Technical Conference (Santa Clara, CA USA) (USENIX ATC '17). 221\u2013233","author":"Dall Christoffer","year":"2017","unstructured":"Christoffer Dall, Shih-Wei Li, and Jason Nieh. 2017. Optimizing the Design and Implementation of the Linux ARM Hypervisor. In Proceedings of the 2017 USENIX Annual Technical Conference (Santa Clara, CA USA) (USENIX ATC '17). 221\u2013233."},{"key":"e_1_3_2_1_21_1","volume-title":"Supporting KVM on the ARM Architecture. LWN Weekly Edition (July","author":"Dall Christoffer","year":"2013","unstructured":"Christoffer Dall and Jason Nieh. 2013. Supporting KVM on the ARM Architecture. LWN Weekly Edition (July 2013), 18-22."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_25_1","unstructured":"Defense Advanced Research Projects Agency. 2025. V-SPELLS: Verified Security and Performance Enhancement of Large Legacy Software. https:\/\/www.darpa.mil\/research\/programs\/verified-security-and-performance-enhancement-of-large-legacy-software. Accessed 1 Aug. 2025."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586040"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation","author":"Shankaranarayana Gopal Amogha Udupa","year":"2023","unstructured":"Amogha Udupa Shankaranarayana Gopal, Raveendra Soori, Michael Ferdman, and Dongyoon Lee. 2023. TailCheck: A Lightweight Heap Overflow Detection Mechanism with Page Protection and Tagged Pointers. In Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (Boston, MA USA) (OSDI '23). 535-552."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (Savannah, GA USA) (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 Symposium on Operating Systems Design and Implementation (Savannah, GA USA) (OSDI '16). 653\u2013669."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180448"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598034"},{"key":"e_1_3_2_1_38_1","volume-title":"AMD SEV-SNP: Strengthening VM Isolation with Integrity Protection and More. White Paper. Advanced Micro Devices","author":"Kaplan David","unstructured":"David Kaplan, Jeremy Powell, and Tom Woller. 2020. AMD SEV-SNP: Strengthening VM Isolation with Integrity Protection and More. White Paper. Advanced Micro Devices, Inc."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_14"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification","author":"Kupferman Orna","unstructured":"Orna Kupferman and Moshe Y. Vardi. 1999. Model Checking of Safety Properties. In Proceedings of the 11th International Conference on Computer Aided Verification (Trento, Italy) (CAV '99). Springer-Verlag, 172\u2013183."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_45_1","first-page":"1","volume-title":"Proceedings of the BSDCan 2008","volume":"5","author":"Lattner Chris","year":"2008","unstructured":"Chris Lattner. 2008. LLVM and Clang: Next Generation Compiler Technology. In Proceedings of the BSDCan 2008 (Ottawa, ON Canada), Vol. 5. 1-20."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498681"},{"key":"e_1_3_2_1_49_1","unstructured":"Xavier Leroy Andrew W Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Ph.D. Dissertation. Inria."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040319"},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 28th USENIX Security Symposium (Santa Clara, CA USA) (USENIX Security '19)","author":"Li Shih-Wei","year":"2019","unstructured":"Shih-Wei Li, John S. Koh, and Jason Nieh. 2019. Protecting Cloud Virtual Machines from Commodity Hypervisor and Host Operating System Exploits. In Proceedings of the 28th USENIX Security Symposium (Santa Clara, CA USA) (USENIX Security '19). 1357\u20131374."},{"key":"e_1_3_2_1_52_1","unstructured":"Shih-Wei Li Xupeng Li Ronghui Gu Jason Nieh and John Zhuang Hui. 2020. Microverification of the Linux KVM Hypervisor: Proving VM Confidentiality and Integrity. Technical Report CUCS-003-20. Department of Computer Science Columbia University."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the 30th USENIX Security Symposium","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021b. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In Proceedings of the 30th USENIX Security Symposium (Vancouver, BC Canada) (USENIX Security '21). 3953-3970."},{"key":"e_1_3_2_1_55_1","first-page":"465","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (Carlsbad, CA USA) (OSDI '22)","author":"Li Xupeng","year":"2022","unstructured":"Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (Carlsbad, CA USA) (OSDI '22). USA, 465-484."},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation","author":"Li Xupeng","year":"2023","unstructured":"Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. 2023. Spoq: Scaling Machine-Checkable Systems Verification in Coq. In Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (Boston, MA USA) (OSDI '23). 851-869."},{"key":"e_1_3_2_1_57_1","volume-title":"Specification Projections: Scaling Formal Verification of Security Properties for Unmodified System Software. Technical Report CUCS-003-25. Department of Computer Science","author":"Li Xuheng","year":"2025","unstructured":"Xuheng Li, Xupeng Li, Wei Qiang, Ganxiang Yang, Yi Rong, Ronghui Gu, and Jason Nieh. 2025. Specification Projections: Scaling Formal Verification of Security Properties for Unmodified System Software. Technical Report CUCS-003-25. Department of Computer Science, Columbia University."},{"key":"e_1_3_2_1_58_1","volume-title":"https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/. Accessed","author":"Limited Arm","year":"2025","unstructured":"Arm Limited and Contributors. 2023. Trusted Firmware-A. https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/. Accessed 22 Dec. 2025."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371088"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1987.10009"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168607"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_9"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503302"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001434"},{"key":"e_1_3_2_1_70_1","unstructured":"John Rushby. 1992. Noninterference Transitivity and Channel-Control Security Policies. Technical Report CSL-92-02. Computer Science Laboratory SRI International."},{"key":"e_1_3_2_1_71_1","volume-title":"Proceedings of the 8th International Conference on Learning Representations (ICLR","author":"Ryan Gabriel","year":"2020","unstructured":"Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In Proceedings of the 8th International Conference on Learning Representations (ICLR 2020)."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_1_73_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (Savannah, GA USA) (OSDI '16)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (Savannah, GA USA) (OSDI '16). 1\u201316."},{"key":"e_1_3_2_1_74_1","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (Carlsbad, CA USA) (OSDI '18)","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. 2018. Nickel: A Framework for Design and Verification of Information Flow Control Systems. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (Carlsbad, CA USA) (OSDI '18). 287\u2013305."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-44599-1_13"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134098"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454029"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_3_2_1_80_1","first-page":"411","volume-title":"Quantum Virtual Machines. In 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25)","author":"Tao Runzhou","year":"2025","unstructured":"Runzhou Tao, Hongzheng Zhu, Jason Nieh, Jianan Yao, and Ronghui Gu. 2025. Quantum Virtual Machines. In 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25). 411-428."},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2025.241301"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385986"},{"key":"e_1_3_2_1_83_1","first-page":"485","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (Carlsbad, CA USA) (OSDI '22)","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (Carlsbad, CA USA) (OSDI '22). 485-501."},{"key":"e_1_3_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632877"},{"key":"e_1_3_2_1_85_1","first-page":"405","volume-title":"Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (Santa Clara, CA USA) (OSDI '21)","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation (Santa Clara, CA USA) (OSDI '21). 405-421."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"e_1_3_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"ASPLOS '26: 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Pittsburgh PA USA","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGARCH ACM Special Interest Group on Computer Architecture","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3779212.3790171","content-type":"text\/html","content-version":"vor","intended-application":"syndication"}],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T14:03:01Z","timestamp":1773583381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779212.3790171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,22]]},"references-count":87,"alternative-id":["10.1145\/3779212.3790171","10.1145\/3779212"],"URL":"https:\/\/doi.org\/10.1145\/3779212.3790171","relation":{},"subject":[],"published":{"date-parts":[[2026,3,22]]},"assertion":[{"value":"2026-03-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}