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.
Proving a kernel's memory management correct, and what such a proof leaves out. Collects the machine-checked kernel verifications together with the memory models they must stand on. Membership requires the proof to reach memory management specifically; a verified component above it belongs elsewhere.
8 references
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
Lessons Learned From Microkernel Verification — Specification is the New Bottleneck
Christoph Baumann and others (2012) · Systems Software Verification Conference 2012 (SSV 2012) · Open Publishing Association
Verification of programs in virtual memory using separation logic
Rafal Michal Kolanski (2011) · UNSW Sydney
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
Types, bytes, and separation logic
Harvey Tuch and others (2007) · 34th ACM Symposium on Principles of Programming Languages (POPL)