Modal Verification Patterns for Systems Software
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866912610857779200 |
|---|---|
| author | Kuru, Ismail Gordon, Colin S. |
| author_facet | Kuru, Ismail Gordon, Colin S. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_01719 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Modal Verification Patterns for Systems Software Kuru, Ismail Gordon, Colin S. Logic in Computer Science D.2.1; D.2.4; D.3.1; E.1 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. |
| title | Modal Verification Patterns for Systems Software |
| topic | Logic in Computer Science D.2.1; D.2.4; D.3.1; E.1 |
| url | https://arxiv.org/abs/2506.01719 |