On Verification Patterns for Low-Level Systems via Modal Abstractions

Kuru, Ismail, Gordon, Colin S.

Proceedings of the 13th Workshop on Programming Languages and Operating Systems (PLOS 2025), October 2025

Abstract

Although they differ in the functionality they offer, low-level systems exhibit certain patterns of design and utilization of computing resources. In this paper we examine how modalities have emerged as a common structure in formal verification of low-level software, and explain how many recent examples naturally share common structure in the relationship between the modalities and software features they are used to reason about. We explain how the concept of a resource context (a class of system resources to reason about) naturally corresponds to families of modal operators indexed by system data, and how this naturally leads to using modal assertions to describe resource elements (data in the relevant context). We also describe extensions of this idea to ongoing work in formal verification of filesystems code.

Bibtex

@inproceedings{plos25,
    title = {On Verification Patterns for Low-Level Systems via Modal
             Abstractions},
    author = {Kuru, Ismail and Gordon, Colin S.},
    booktitle = {Proceedings of the 13th Workshop on Programming Languages and
                 Operating Systems (PLOS 2025)},
    year = {2025},
    address = {Seoul, South Korea},
    note = {To Appear..},
abstract = {
Although they differ in the functionality they offer, low-level
systems exhibit certain patterns of design and utilization of computing
resources.

In this paper we examine how modalities have emerged as a common
structure in formal verification of low-level software, and explain how many
recent examples naturally share common structure in the relationship
between the modalities and software features they are used to reason
about. We explain how the concept of a resource context (a class of
system resources to reason about) naturally corresponds to families of
modal operators indexed by system data, and how this naturally leads to
using modal assertions to describe resource elements (data in the relevant
context). We also describe extensions of this idea to ongoing work in
formal verification of filesystems code.
}
}