Atmosphere: Towards Practical Verified Kernels in Rust
Published in KISV '23: Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification
This work applies a linearly typed extension of Rust and a newly developed SMT Verifier, Verus, to formally verify low-level operating system code.
Citation: Atmosphere: Towards Practical Verified Kernels in Rust. Xiangdong C., Zhaofeng L., Mesicek L., Narayanan V., and Burtsev A. Published in KISV '23: Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification.
Read MoreCategories: Formal Verification