{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T15:31:37Z","timestamp":1773588697973,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":82,"publisher":"ACM","funder":[{"name":"Samsung Research","award":["0"],"award-info":[{"award-number":["0"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,3,22]]},"DOI":"10.1145\/3779212.3790152","type":"proceedings-article","created":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T13:55:26Z","timestamp":1773150926000},"page":"583-601","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Detecting Inconsistencies in Arm CCA's Formally Verified Specification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5409-8718","authenticated-orcid":false,"given":"Changho","family":"Choi","sequence":"first","affiliation":[{"name":"Samsung Research, Seoul, Republic of Korea"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0066-9608","authenticated-orcid":false,"given":"Xiang","family":"Cheng","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, Atlanta, GA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6993-3524","authenticated-orcid":false,"given":"Bokdeuk","family":"Jeong","sequence":"additional","affiliation":[{"name":"Samsung Research, Seoul, Republic of Korea"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7440-2067","authenticated-orcid":false,"given":"Taesoo","family":"Kim","sequence":"additional","affiliation":[{"name":"Samsung Research, Seoul, Republic of Korea and Georgia Institute of Technology, Atlanta, GA, USA"}]}],"member":"320","published-online":{"date-parts":[[2026,3,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 34th IEEE Symposium on Security and Privacy (Oakland)","unstructured":"2013. Proceedings of the 34th IEEE Symposium on Security and Privacy (Oakland). San Francisco, CA."},{"key":"e_1_3_2_1_2_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","unstructured":"2016. Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 25th USENIX Security Symposium (Security)","unstructured":"2016. Proceedings of the 25th USENIX Security Symposium (Security). Austin, TX."},{"key":"e_1_3_2_1_4_1","volume-title":"Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP)","unstructured":"2017. Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP). Shanghai, China."},{"key":"e_1_3_2_1_5_1","unstructured":"Arm 2021. DEN0096: Arm CCA Security Model. Arm. Accessed: 2025-08-08."},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","unstructured":"2022. Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Carlsbad, CA."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 38th Annual ACMConference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)","unstructured":"2023. Proceedings of the 38th Annual ACMConference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). Cascais, Portugal."},{"key":"e_1_3_2_1_8_1","unstructured":"Arm 2024. DEN0137: Realm Management Monitor specification. Arm. Accessed: 2025-08-08."},{"key":"e_1_3_2_1_9_1","unstructured":"Arm 2025. DDI0626: Architecture Specification Language Reference. Arm. Accessed: 2025-08-05."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_11_1","volume-title":"https:\/\/www.anthropic.com\/news\/claude-3-7-sonnet. Introduced extended thinking mode for advanced reasoning and problem-solving, with a context window of up to 128,000 tokens. Knowledge cutoff","author":"Sonnet Claude","year":"2024","unstructured":"Anthropic. 2025. Claude 3.7 Sonnet. https:\/\/www.anthropic.com\/news\/claude-3-7-sonnet. Introduced extended thinking mode for advanced reasoning and problem-solving, with a context window of up to 128,000 tokens. Knowledge cutoff: October 2024.."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 4th International Conference on Formal Methods for Components and Objects (FMCO)","author":"Barnett Mike","year":"2005","unstructured":"Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: a modular reusable verifier for objectoriented programs. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects (FMCO) (Amsterdam, The Netherlands). Berlin, Heidelberg."},{"key":"e_1_3_2_1_14_1","unstructured":"Aditya Bhuyan. 2024. How Arm's Success in Data Centers is Shaping the Future of Chip Technology. https:\/\/aditya-sunjava.medium.com\/how-arms-success-in-data-centers-is-shaping-the-future-of-chiptechnology-50a7748861f7. [Online; accessed: 7-Aug-2025]."},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 14th International Conference on Computer Aided Verification (CAV)","author":"Bryant Randal E.","unstructured":"Randal E. Bryant, Shuvendu K. Lahiri, and Sanjit A. Seshia. 2002. Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV). Copenhagen, Denmark."},{"key":"e_1_3_2_1_16_1","unstructured":"Tej Chajed Joseph Tassarotti Mark Theng M. Frans Kaashoek and Nickolai Zeldovich. 2022. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning See [6]."},{"key":"e_1_3_2_1_17_1","volume-title":"Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich.","author":"Chen Haogang","year":"2017","unstructured":"Haogang Chen, Tej Chajed, Alex Konradi, Stephanie Wang, Atalay undefinedleri, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2017. Verifying a high-performance crash-safe file system using a tree specification, See [4]."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_19_1","volume-title":"Hao Yu, Nan Duan, Peng Cheng, et al.","author":"Chen Tianyu","year":"2024","unstructured":"Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong, Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Hao Yu, Nan Duan, Peng Cheng, et al. 2024. Automated Proof Generation for Rust Code via Self-Evolution. arXiv preprint arXiv:2410.15756 (2024)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3731569.3764821"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the 32nd USENIX Security Symposium (Security)","author":"Chen Yi","year":"2023","unstructured":"Yi Chen, Di Tang, Yepeng Yao, Mingming Zha, XiaoFeng Wang, Xiaozhong Liu, Haixu Tang, and Baoxu Liu. 2023. Sherlock on Specs: Building LTE Conformance Tests through Automated Reasoning. In Proceedings of the 32nd USENIX Security Symposium (Security). Anaheim, CA."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_2_1_23_1","unstructured":"Victor Costan Ilia Lebedev and Srinivas Devadas. 2016. Sanctum: minimal hardware extensions for strong software isolation See [3]."},{"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","volume-title":"DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. https:\/\/arxiv.org\/abs\/2501.129 48. Released","author":"DeepSeek AI.","year":"2025","unstructured":"DeepSeek AI. 2025. DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning. https:\/\/arxiv.org\/abs\/2501.129 48. Released in January 2025. Achieves performance comparable to OpenAI-o1-1217 on reasoning tasks, leveraging multi-stage training and cold-start data.."},{"key":"e_1_3_2_1_26_1","first-page":"60","volume-title":"Proceedings of the 2006 ACM SIGPLAN Workshop on Haskell (Haskell '06)","author":"Derrin Philip","unstructured":"Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. 2006. Running the manual: an approach to high-assurance microkernel development. In Proceedings of the 2006 ACM SIGPLAN Workshop on Haskell (Haskell '06). New York, NY, 60-71."},{"key":"e_1_3_2_1_27_1","volume-title":"Komodo: Using verification to disentangle secure-enclave hardware from software, See [4].","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. 2017. Komodo: Using verification to disentangle secure-enclave hardware from software, See [4]."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064183"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_2"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP)","author":"Fox Anthony","unstructured":"Anthony Fox and Magnus O. Myreen. 2010. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP). Edinburgh, UK."},{"key":"e_1_3_2_1_32_1","unstructured":"Anthony C. J. Fox Gareth Stockwell Shale Xiong Hanno Becker Dominic P. Mulligan Gustavo Petri and Nathan Chong. 2023. A Verification Methodology for the Arm\u00ae Confidential Computing Architecture: From a Secure Specification to Safe Implementations See [7]."},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design (FMCAD)","author":"Gao Dapeng","year":"2021","unstructured":"Dapeng Gao and Tom Melham. 2021. End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design (FMCAD). Virtual Event, CT."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682944"},{"key":"e_1_3_2_1_35_1","volume-title":"Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Goldweber Eli","year":"2024","unstructured":"Eli Goldweber, Weixin Yu, Seyed Armin Vakil Ghahani, and Manos Kapritsos. 2024. IronSpec: Increasing the Reliability of Formal Specifications. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Santa Clara, CA."},{"key":"e_1_3_2_1_36_1","unstructured":"Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels See [2]."},{"key":"e_1_3_2_1_37_1","volume-title":"Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to- End Security via Automated Full-System Verification. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, Colorado."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231535"},{"key":"e_1_3_2_1_39_1","unstructured":"Uri Kirstein. 2022. Post-Mortem Analysis of the Notional Finance Vulnerability \u2014 A Tautological Invariant. https:\/\/medium.com\/certora\/post-mortem-analysis-of-the-notional-finance-vulnerability-atautological-invariant-574d02d6ac15. [Online; accessed: 7-Aug-2025]."},{"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","volume-title":"Decision Procedures: An Algorithmic Point of View","author":"Kroening Daniel","year":"2008","unstructured":"Daniel Kroening and Ofer Strichman. 2008. Decision Procedures: An Algorithmic Point of View. Springer Publishing Company, Incorporated."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_2_1_43_1","volume-title":"Verus: Verifying Rust Programs using Linear Ghost Types, See [7].","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types, See [7]."},{"key":"e_1_3_2_1_44_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, Edmund M. Clarke and Andrei Voronkov (Eds.). Berlin, Heidelberg, 348-370."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_46_1","volume-title":"SpecLLM: Exploring Generation and Review of VLSI Design Specification with Large Language Model. arXiv preprint arXiv:2401.13266","author":"Li Mengming","year":"2024","unstructured":"Mengming Li, Wenji Fang, Qijun Zhang, and Zhiyao Xie. 2024. SpecLLM: Exploring Generation and Review of VLSI Design Specification with Large Language Model. arXiv preprint arXiv:2401.13266 (2024)."},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the 30th USENIX Security Symposium (Security)","author":"Li Shih-Wei","year":"2021","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 Proceedings of the 30th USENIX Security Symposium (Security). Virtual Event, Canada."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_49_1","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 See [6]."},{"key":"e_1_3_2_1_50_1","volume-title":"SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. arXiv preprint arXiv:2401.08807","author":"Ma Lezhi","year":"2024","unstructured":"Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2024. SpecGen: Automated Generation of Formal Program Specifications via Large Language Models. arXiv preprint arXiv:2401.08807 (2024)."},{"key":"e_1_3_2_1_51_1","volume-title":"Released on","author":"Meta","year":"2024","unstructured":"Meta AI. 2024. Llama 3.1 70B. https:\/\/ai.meta.com\/llama\/. Released on July 23, 2024."},{"key":"e_1_3_2_1_52_1","volume-title":"FBSDetector: Fake Base Station and Multi Step Attack Detection in Cellular Networks using Machine Learning. arXiv preprint arXiv:2401.04958","author":"Mubasshir Kazi Samin","year":"2024","unstructured":"Kazi Samin Mubasshir, Imtiaz Karim, and Elisa Bertino. 2024. FBSDetector: Fake Base Station and Multi Step Attack Detection in Cellular Networks using Machine Learning. arXiv preprint arXiv:2401.04958 (2024)."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Toby Murray Daniel Matichuk Matthew Brassil Peter Gammie Timothy Bourke Sean Seefried Corey Lewis Xin Gao and Gerwin Klein. 2013. seL4: From General Purpose to a Proof of Information Flow Enforcement See [1].","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00055"},{"key":"e_1_3_2_1_56_1","volume-title":"Released on","author":"AI.","year":"2024","unstructured":"OpenAI. 2024. GPT-4o. https:\/\/openai.com\/gpt-4o. Released on May 13, 2024. Multimodal AI model integrating text, voice, and vision capabilities.."},{"key":"e_1_3_2_1_57_1","volume-title":"https:\/\/openai.com\/index\/openai-o1-systemcard\/. Released on","author":"AI.","year":"2024","unstructured":"OpenAI. 2024. GPT-o1. https:\/\/openai.com\/index\/openai-o1-systemcard\/. Released on December 5, 2024. Reflective generative pretrained transformer with enhanced reasoning capabilities in STEM, programming, and complex tasks.."},{"key":"e_1_3_2_1_58_1","volume-title":"Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 1022-1034","author":"Park Jihyeok","year":"2022","unstructured":"Jihyeok Park, Seungmin An, and Sukyoung Ryu. 2022. Automatically deriving JavaScript static analyzers from specifications using metalevel static analysis. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. 1022-1034."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678781"},{"key":"e_1_3_2_1_60_1","volume-title":"2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 13-24","author":"Park Jihyeok","year":"2021","unstructured":"Jihyeok Park, Seungmin An, Dongjun Youn, Gyeongwon Kim, and Sukyoung Ryu. 2021. Jest: N 1-version differential testing of both javascript engines and specification. In 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE). IEEE, 13-24."},{"key":"e_1_3_2_1_61_1","volume-title":"Proceedings of the 34th International Conference on Computer Aided Verification (CAV)","author":"Polgreen Elizabeth","unstructured":"Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. 2022. UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis. In Proceedings of the 34th International Conference on Computer Aided Verification (CAV). Haifa, Israel."},{"key":"e_1_3_2_1_62_1","first-page":"5215","volume-title":"33rd USENIX Security Symposium (USENIX Security 24)","author":"Rahman Mirza Masfiqur","year":"2024","unstructured":"Mirza Masfiqur Rahman, Imtiaz Karim, and Elisa Bertino. 2024. CellularLint: A Systematic Approach to Identify Inconsistent Behavior in Cellular Network Specifications. In 33rd USENIX Security Symposium (USENIX Security 24). 5215-5232."},{"key":"e_1_3_2_1_63_1","volume-title":"Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. 2102-2116","author":"Mukit Rashid Syed Md","year":"2024","unstructured":"Syed Md Mukit Rashid, Tianwei Wu, Kai Tu, Abdullah Al Ishtiaq, Ridwanul Hasan Tanvir, Yilu Dong, Omar Chowdhury, and Syed Rafiul Hussain. 2024. State Machine Mutation-based Testing Framework for Wireless Communication Protocols. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. 2102-2116."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077658"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133912"},{"key":"e_1_3_2_1_66_1","volume-title":"Proceedings of the 28th International Conference on Computer Aided Verification (CAV)","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. 2016. End-to-End Verification of Processors with ISA-Formal. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV). Toronto, Canada."},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3346501"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_3_2_1_70_1","unstructured":"Helgi Sigurbjarnarson James Bornholt Emina Torlak and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement See [2]."},{"key":"e_1_3_2_1_71_1","volume-title":"Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS)","author":"Subramanyan Pramod","unstructured":"Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas Devadas, and Sanjit A. Seshia. 2017. A Formal Foundation for Secure Remote Execution of Enclaves. In Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS). Dallas, TX."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"crossref","unstructured":"Amit Vasudevan Sagar Chaki Limin Jia Jonathan McCune James Newsome and Anupam Datta. 2013. Design Implementation and Verification of an eXtensible and Modular Hypervisor Framework See [1].","DOI":"10.1109\/SP.2013.36"},{"key":"e_1_3_2_1_74_1","unstructured":"Amit Vasudevan Sagar Chaki Petros Maniatis Limin Jia and Anupam Datta. 2016. \u00fcberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor See [3]."},{"key":"e_1_3_2_1_75_1","volume-title":"Critical Bug Payout Report. https:\/\/blog.notional.finance\/critical-bug-payout-report. [Online","author":"Jeff Wu.","year":"2025","unstructured":"Jeff Wu. 2022. Critical Bug Payout Report. https:\/\/blog.notional.finance\/critical-bug-payout-report. [Online; accessed: 7-Aug-2025]."},{"key":"e_1_3_2_1_76_1","volume-title":"Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al.","author":"Yang Chenyuan","year":"2024","unstructured":"Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R Lorch, Shuai Lu, et al. 2024. AutoVerus: Automated proof generation for Rust code. arXiv preprint arXiv:2409.13082 (2024)."},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_1_78_1","volume-title":"WEST: Specification-Based Test Generation for WebAssembly. In 2025 40th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE\/ACM.","author":"Youn Dongjun","year":"2025","unstructured":"Dongjun Youn, Wonho Shin, and Sukyoung Ryu. 2025. WEST: Specification-Based Test Generation for WebAssembly. In 2025 40th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE\/ACM."},{"key":"e_1_3_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359647"},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613153"},{"key":"e_1_3_2_1_82_1","volume-title":"RAGVerus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation. arXiv preprint arXiv:2502.05344","author":"Zhong Sicheng","year":"2025","unstructured":"Sicheng Zhong, Jiading Zhu, Yifang Tian, and Xujie Si. 2025. RAGVerus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation. arXiv preprint arXiv:2502.05344 (2025)."}],"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":[],"deposited":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T14:07:07Z","timestamp":1773583627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779212.3790152"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,22]]},"references-count":82,"alternative-id":["10.1145\/3779212.3790152","10.1145\/3779212"],"URL":"https:\/\/doi.org\/10.1145\/3779212.3790152","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"}}]}}