Kuru, Ismail, Gordon, Colin S.
Proceedings of the 13th Workshop on Programming Languages and Operating Systems (PLOS 2025), October 2025
Abstract
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.
}
}