Modal Verification Patterns for Systems Software

Kuru, Ismail, Gordon, Colin S.

Proceedings of the 13th Workshop on Programming Languages and Operating Systems (PLOS 2025), October 2025, doi: 10.1145/3764860.3768337

pdf doi acm

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 = {Modal Verification Patterns for Systems Software},
	author = {Kuru, Ismail and Gordon, Colin S.},
	booktitle = {Proceedings of the 13th Workshop on Programming Languages and
	             Operating Systems (PLOS 2025)},
	year = {2025},
	doi = {10.1145/3764860.3768337},
	acm = {https://dl.acm.org/doi/10.1145/3764860.3768337},
	address = {Seoul, South Korea},
	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. },
}