{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:43Z","timestamp":1780994563016,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["EP\/Y035976\/1 SAFER"],"award-info":[{"award-number":["EP\/Y035976\/1 SAFER"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["789108"],"award-info":[{"award-number":["789108"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101189371"],"award-info":[{"award-number":["101189371"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006041","name":"Innovate UK","doi-asserted-by":"publisher","award":["DSbD 105694"],"award-info":[{"award-number":["DSbD 105694"]}],"id":[{"id":"10.13039\/501100006041","id-type":"DOI","asserted-by":"publisher"}]},{"name":"EPSRC","award":["EP\/Z000580\/1"],"award-info":[{"award-number":["EP\/Z000580\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764817","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"685-700","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3723-636X","authenticated-orcid":false,"given":"Kayvan","family":"Memarian","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-8431-9577","authenticated-orcid":false,"given":"Ben","family":"Simner","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4506-6236","authenticated-orcid":false,"given":"David","family":"Kaloper-Mer\u0161injak","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0005-7618","authenticated-orcid":false,"given":"Thibaut","family":"P\u00e9rami","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015","author":"Amit Nadav","year":"2015","unstructured":"Nadav Amit, Dan Tsafrir, Assaf Schuster, Ahmad Ayoub, and Eran Shlomo. 2015. Virtual CPU validation. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, Ethan L. Miller and Steven Hand (Eds.). ACM, 311\u2013327. 10.1145\/2815400.2815420"},{"key":"e_1_3_2_1_2_1","volume-title":"Summers","author":"Astrauskas Vytautas","year":"2022","unstructured":"Vytautas Astrauskas, Aurel B\u00edl\u00fd, Jon\u00e1s Fiala, Zachary Grannan, Christoph Matheja, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2022. The Prusti Project: Formal Verification for Rust. In NFM (Lecture Notes in Computer Science, Vol. 13260). Springer, 88\u2013108."},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. ACM Program. Lang. 9, POPL","author":"Banerjee Rini","year":"2025","unstructured":"Rini Banerjee, Kayvan Memarian, Dhruv C. Makwana, Christopher Pulte, Neel Krishnaswami, and Peter Sewell. 2025. Fulminate: Testing CN Separation-Logic Specifications in C. Proc. ACM Program. Lang. 9, POPL (2025), 1260\u20131292. 10.1145\/3704879"},{"key":"e_1_3_2_1_4_1","volume-title":"Robert DeLine, Bart Jacobs, and K. Rustan M. Leino.","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In FMCO (Lecture Notes in Computer Science, Vol. 4111). Springer, 364\u2013387."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243650"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243650"},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the ACM SIGCOMM 2005 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications","author":"Bishop Steve","year":"2005","unstructured":"Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. 2005. Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets. In Proceedings of the ACM SIGCOMM 2005 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Philadelphia, Pennsylvania, USA, August 22-26, 2005, Roch Gu\u00e9rin, Ramesh Govindan, and Greg Minshall (Eds.). ACM, 265\u2013276. 10.1145\/1080091.1080123"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-009-9148-3"},{"key":"e_1_3_2_1_9_1","volume-title":"SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz","author":"Bornholt James","year":"2021","unstructured":"James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. 2021. Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. In SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz, Germany, October 26-29, 2021, Robbert van Renesse and Nickolai Zeldovich (Eds.). ACM, 836\u2013850. 10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_10_1","volume-title":"Linux Plumbers Conference Android Microconference.","author":"Brazdil David","year":"2022","unstructured":"David Brazdil and Serban Constantinescu. 2022. Android Virtualization Framework \u2014 Protected computing for the next generation use cases. presented at the Linux Plumbers Conference Android Microconference."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024","author":"Cebeci Can","year":"2024","unstructured":"Can Cebeci, Yong-Hao Zou, Diyu Zhou, George Candea, and Cl\u00e9ment Pit-Claudel. 2024. Practical Verification of System-Software Components Written in Standard C. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024, Emmett Witchel, Christopher J. Rossbach, Andrea C. Arpaci-Dusseau, and Kimberly Keeton (Eds.). ACM, 455\u2013472. 10.1145\/3694715.3695980"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1002\/SPE.2949"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00)","author":"Claessen Koen","year":"2000","unstructured":"Koen Claessen and John Hughes. 2000. QuickCheck: a lightweight tool for random testing of Haskell programs. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, 268\u2013279. 10.1145\/351240.351266"},{"key":"e_1_3_2_1_15_1","volume-title":"SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings. 233\u2013247","author":"Cuoq Pascal","year":"2012","unstructured":"Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-C \u2013 A Software Analysis Perspective. In Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings. 233\u2013247. 10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_16_1","volume-title":"Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13","author":"Delahaye Micka\u00ebl","year":"2013","unstructured":"Micka\u00ebl Delahaye, Nikolai Kosmatov, and Julien Signoles. 2013. Common specification language for static and dynamic analysis of C programs. In Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, Coimbra, Portugal, March 18-22, 2013, Sung Y. Shin and Jos\u00e9 Carlos Maldonado (Eds.). ACM, 1230\u20131235. 10.1145\/2480362.2480593"},{"key":"e_1_3_2_1_17_1","volume-title":"How We Built Cedar: A Verification-Guided Approach. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, FSE 2024, Porto de Galinhas","author":"Disselkoen Craig","year":"2024","unstructured":"Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John H. Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, and Andrew Wells. 2024. How We Built Cedar: A Verification-Guided Approach. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, FSE 2024, Porto de Galinhas, Brazil, July 15-19, 2024, Marcelo d'Amorim (Ed.). ACM, 351\u2013357. 10.1145\/3663529.3663854"},{"key":"e_1_3_2_1_18_1","volume-title":"Proceedings of the Thirteenth EuroSys Conference, EuroSys 2018","author":"Fonseca Pedro","year":"2018","unstructured":"Pedro Fonseca, Xi Wang, and Arvind Krishnamurthy. 2018. MultiNyx: a multi-level abstraction framework for systematic analysis of hypervisors. In Proceedings of the Thirteenth EuroSys Conference, EuroSys 2018, Porto, Portugal, April 23-26, 2018, Rui Oliveira, Pascal Felber, and Y. Charlie Hu (Eds.). ACM, 23:1\u201323:12. 10.1145\/3190508.3190529"},{"key":"e_1_3_2_1_19_1","unstructured":"Google LLC. 2024. Android Virtualization Framework (AVF) overview. https:\/\/source.android.com\/docs\/core\/virtualization Accessed 2024-11-11."},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Gu Ronghui","year":"2015","unstructured":"Ronghui Gu, J\u00e9r\u00e9mie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL '15). ACM, New York, NY, USA, 595\u2013608. 10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_21_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","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. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael Lowell Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, Ethan L. Miller and Steven Hand (Eds.). ACM, 1\u201317. 10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_23_1","unstructured":"D. Jackson and J. Wing. 1996. Lightweight Formal Methods. IEEE Computer (April 1996) 21\u201322."},{"key":"e_1_3_2_1_24_1","volume-title":"Sound, Predictable, Fast Verifier for C and Java","author":"Jacobs Bart","unstructured":"Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 41\u201355."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242380"},{"key":"e_1_3_2_1_26_1","volume-title":"CiE 2017, Turku, Finland, June 12-16, 2017, Proceedings (Lecture Notes in Computer Science","volume":"41","author":"Jones Cliff B.","year":"2017","unstructured":"Cliff B. Jones. 2017. Turing's 1949 Paper in Context. In Unveiling Dynamics and Complexity - 13th Conference on Computability in Europe, CiE 2017, Turku, Finland, June 12-16, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10307), Jarkko Kari, Florin Manea, and Ion Petre (Eds.). Springer, 32\u201341. 10.1007\/978-3-319-58741-7_4"},{"key":"e_1_3_2_1_27_1","unstructured":"Dave Kleidermacher. 2024. Why AVF? article in Dave Kleidermacher's blog. https:\/\/davek.substack.com\/p\/why-avf"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/954666.971189"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024","author":"Lattuada Andrea","year":"2024","unstructured":"Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: A Practical Foundation for Systems Verification. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP 2024, Austin, TX, USA, November 4-6, 2024, Emmett Witchel, Christopher J. Rossbach, Andrea C. Arpaci-Dusseau, and Kimberly Keeton (Eds.). ACM, 438\u2013454. 10.1145\/3694715.3695952"},{"key":"e_1_3_2_1_32_1","volume-title":"Proc. ACM Program. Lang. 7, OOPSLA1","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. Proc. ACM Program. Lang. 7, OOPSLA1 (2023), 286\u2013315. 10.1145\/3586037"},{"key":"e_1_3_2_1_33_1","volume-title":"Verifying the Microsoft Hyper-V Hypervisor with VCC. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. 806\u2013809","author":"Leinenbach Dirk","year":"2009","unstructured":"Dirk Leinenbach and Thomas Santen. 2009. Verifying the Microsoft Hyper-V Hypervisor with VCC. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. 806\u2013809. 10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_35_1","volume-title":"30th USENIX Security Symposium, USENIX Security 2021","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 30th USENIX Security Symposium, USENIX Security 2021, August 11-13, 2021, Michael Bailey and Rachel Greenstadt (Eds.). USENIX Association, 3953\u20133970. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-shih-wei"},{"key":"e_1_3_2_1_36_1","volume-title":"2021 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. A Secure and Formally Verified Linux KVM Hypervisor. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, Los Alamitos, CA, USA, 839\u2013856. 10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230345"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3158196"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012","author":"Martignoni Lorenzo","year":"2012","unstructured":"Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. 2012. Path-exploration lifting: hi-fi tests for lo-fi emulators. In Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2012, London, UK, March 3-7, 2012, Tim Harris and Michael L. Scott (Eds.). ACM, 337\u2013348. 10.1145\/2150976.2151012"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, ISSTA 2009","author":"Martignoni Lorenzo","year":"2009","unstructured":"Lorenzo Martignoni, Roberto Paleari, Giampaolo Fresi Roglia, and Danilo Bruschi. 2009. Testing CPU emulators. In Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, ISSTA 2009, Chicago, IL, USA, July 19-23, 2009, Gregg Rothermel and Laura K. Dillon (Eds.). ACM, 261\u2013272. 10.1145\/1572272.1572303"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON","author":"Nelson Luke","year":"2019","unstructured":"Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, Tim Brecht and Carey Williamson (Eds.). ACM, 225\u2013242. 10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28-31, 2017. ACM, 252\u2013269. 10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023","author":"Ni Haobin","year":"2023","unstructured":"Haobin Ni, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Tahina Ramananandro, and Nikhil Swamy. 2023. ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). ACM, 275\u2013289. 10.1145\/3573105.3575684"},{"key":"e_1_3_2_1_45_1","unstructured":"Sandeep Patil and Irene Ang. 2023. Virtual Machine as a core Android Primitive. article in the Android Developers blog. https:\/\/android-developers.googleblog.com\/2023\/12\/virtual-machines-as-core-android-primitive.html"},{"key":"e_1_3_2_1_46_1","volume-title":"Proc. ACM Program. Lang. 7, POPL","author":"Pulte Christopher","year":"2023","unstructured":"Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. 2023. CN: Verifying Systems C Code with Separation-Logic Refinement Types. Proc. ACM Program. Lang. 7, POPL (2023), 1\u201332. 10.1145\/3571194"},{"key":"e_1_3_2_1_47_1","volume-title":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","author":"Sammler Michael","year":"2021","unstructured":"Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021, Stephen N. Freund and Eran Yahav (Eds.). ACM, 158\u2013174. 10.1145\/3453483.3454036"},{"key":"e_1_3_2_1_48_1","series-title":"Lecture Notes in Computer Science","volume-title":"First Steps towards the Certification of an ARM Simulator Using Compcert","author":"Shi Xiaomu","unstructured":"Xiaomu Shi, Jean-Fran\u00e7ois Monin, Fr\u00e9d\u00e9ric Tuong, and Fr\u00e9d\u00e9ric Blanqui. 2011. First Steps towards the Certification of an ARM Simulator Using Compcert. In Certified Programs and Proofs, Jean-Pierre Jouannaud and Zhong Shao (Eds.). Lecture Notes in Computer Science, Vol. 7086. Springer Berlin Heidelberg, 346\u2013361. 10.1007\/978-3-642-25379-9_25"},{"key":"e_1_3_2_1_49_1","unstructured":"Julien Signoles. 2018. From Static Analysis to Runtime Verification with Frama-C and E-ACSL. https:\/\/tel.archives-ouvertes.fr\/tel-04469397"},{"key":"e_1_3_2_1_50_1","volume-title":"VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution","author":"Signoles Julien","year":"2021","unstructured":"Julien Signoles. 2021. The e-ACSL perspective on runtime assertion checking. In VORTEX 2021: Proceedings of the 5th ACM International Workshop on Verification and mOnitoring at Runtime EXecution, Virtual Event, Denmark, 12 July 2021, Wolfgang Ahrendt, Davide Ancona, and Adrian Francalanza (Eds.). ACM, 8\u201312. 10.1145\/3464974.3468451"},{"key":"e_1_3_2_1_51_1","volume-title":"43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256\u2013270","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohou\u00e9, and Santiago Zanella-B\u00e9guelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256\u2013270. https:\/\/www.fstar-lang.org\/papers\/mumon\/"},{"key":"e_1_3_2_1_52_1","volume-title":"SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz","author":"Tao Runzhou","year":"2021","unstructured":"Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu. 2021. Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. In SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event \/ Koblenz, Germany, October 26-29, 2021, Robbert van Renesse and Nickolai Zeldovich (Eds.). ACM, 866\u2013881. 10.1145\/3477132.3483560"},{"key":"e_1_3_2_1_53_1","volume-title":"Report on a Conference on High Speed Automatic Computation","author":"Turing Alan M.","year":"1949","unstructured":"Alan M. Turing. 1949. Checking a Large Routine. In Report on a Conference on High Speed Automatic Computation, June 1949. University Mathematical Laboratory, Cambridge University, Cambridge, UK, 67\u201369. http:\/\/www.turingarchive.org\/browse.php\/B\/8. A corrected version is printed in Morris and Jones, 1984 https:\/\/ieeexplore.ieee.org\/document\/4640518. Accessed 2025-04-10.."},{"key":"e_1_3_2_1_54_1","volume-title":"VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2024, Santa Clara, CA, USA, July 10-12, 2024, Ada Gavrilovska and Douglas B. Terry (Eds.). USENIX Association, 599\u2013614. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/zhou"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:53:35Z","timestamp":1759323215000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764817"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":54,"alternative-id":["10.1145\/3731569.3764817","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764817","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}