@inproceedings{10.1145/3713082.3730387,
author = {Malecha, Gregory and Dang, Hoang-Hai and Giarrusso, Paolo G. and Hudon, Simon and Kaiser, Jan-Oliver and Swasey, David},
title = {Modular, Full-System Verification},
year = {2025},
isbn = {9798400714757},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3713082.3730387},
doi = {10.1145/3713082.3730387},
abstract = {We present an approach to specifying operating systems that is both highly modular and supports deriving various properties necessary to modern operating systems. The approach combines a machine semantics decomposed by privilege levels with a separation logic specification of the operating system API. We describe how the specification style enables natural proofs of robust safety in addition to deep behavioral refinements of user-mode applications running atop the OS. This approach enables simple and flexible concurrent specifications and unlocks new opportunities for whole-system verification.},
booktitle = {Proceedings of the 2025 Workshop on Hot Topics in Operating Systems},
pages = {42–49},
numpages = {8},
keywords = {Formal verification, Iris, Multi-core verification, Operating system specification, Separation logic},
location = {Banff, AB, Canada},
series = {HotOS '25}
}