Preprint
Modal Verification Patterns for Systems
25 Jun 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 argue the position that modalities, in the sense of modal logic, should be a go-to approach when specifying and verifying low-level systems code. We explain how the concept of a resource context helps guide the design of new modalities for verification of systems code, and we justify our perspective by discussing prior systems that have used modalities for systems verification successfully, arguing that they fit into the verification design pattern we articulate, and explaining how this approach might apply to other systems verification challenges.
Metrics
4 Record Views
Details
- Title
- Modal Verification Patterns for Systems
- Creators
- Ismail KuruColin S Gordon
- Resource Type
- Preprint
- Language
- English
- Academic Unit
- Computer Science
- Other Identifier
- 991022059839504721