Logo image
Back
Modal Verification Patterns for Systems Software
Conference proceeding   Open access

Modal Verification Patterns for Systems Software

Ismail Kuru and Colin Stebbins Gordon
PLOS '25: Proceedings of the 13th Workshop on Programming Languages and Operating Systems, pp 25-33
13 Oct 2025
DOI: https://doi.org/10.1145/3764860.3768337
Featured in Collection :   Research Supported by Drexel Libraries' OA Programs
url
https://doi.org/10.1145/3764860.3768337View
Published, Version of Record (VoR)Open Access via Drexel Libraries Read and Publish Program 2025CC BY V4.0,  Open

Abstract

separation logic modal logic verification operating systems
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).

Metrics

11 Record Views

Details

Logo image