This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Verified memory management
A subject the papers are about. The loosest grouping, and the one to reach for last.
Machine-checked proofs of kernel memory management, the memory models they stand on, and what they leave out. Membership: the proof reaches memory management specifically.
19 references
Extending concurrent separation logic to the hardware level to verify the xv6 OS kernel on RISC-V with AI agents
Kaashoek, M. Frans and others (2026)
Puss in Boots: Formalizing Arm’s Virtual Memory System Architecture
Jade Alglave and others (2024) · Institute of Electrical and Electronics Engineers (IEEE)
Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor
Zhenyang Dai and others (2024) · Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2
Verified Paging for x86-64 in Rust
Matthias Brun (2022) · ETH Zurich
Relaxed virtual memory in Armv8-A
Ben Simner and others (2022) · Programming Languages and Systems · Springer International Publishing
Formal Reasoning Under Cached Address Translation
Hira Taqdees Syeda and others (2020) · Journal of Automated Reasoning · Springer Science and Business Media LLC
Low-level program verification under cached address translation
Hira Taqdees Syeda (2019)
Program Verification in the Presence of Cached Address Translation
Hira Taqdees Syeda and others (2018) · Springer International Publishing
Verification of programs in virtual memory using separation logic
Rafal Michal Kolanski (2011) · UNSW Sydney
Address Translation Aware Memory Consistency
Bogdan Romanescu and others (2010) · IEEE Micro · Institute of Electrical and Electronics Engineers (IEEE)
Specifying and dynamically verifying address translation-aware memory consistency
Bogdan F. Romanescu and others (2010)
Formal verification of demand paging
Artem Starostin (2010) · Universität des Saarlandes
seL4: Formal Verification of an OS Kernel
Gerwin Klein and others (2009) · Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles · Association for Computing Machinery
Formal pervasive verification of a paging mechanism
Eyad Alkassar and others (2008) · International Conference on Tools and Algorithms for the Construction and Analysis of Systems · Springer
A Logic for Virtual Memory
Rafal Kolanski (2008) · Electronic Notes in Theoretical Computer Science · Elsevier BV
Types, bytes, and separation logic
Harvey Tuch and others (2007) · 34th ACM Symposium on Principles of Programming Languages (POPL)
Formal Verification of a Processor with Memory Management Units
Iakov Dalinger (2006)
On the Verification of Memory Management Mechanisms
Iakov Dalinger and others (2005) · Lecture notes in computer science · Springer Science+Business Media
Address Spaces and Virtual Memory: Specification, Implementation, and Correctness
Mark Hillebrand (2005)