Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918345078472704 |
|---|---|
| author | Tobler, James Smith, Graeme |
| author_facet | Tobler, James Smith, Graeme |
| contents | Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_17142 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Generating Rely-Guarantee Conditions with the Conditional-Writes Domain Tobler, James Smith, Graeme Logic in Computer Science Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, in the form of rely-guarantee conditions, conforming to a user-chosen structure. In this work, we introduce one such structure called the conditional-writes domain, designed for programs where it suffices to establish only the conditions under which particular variables are written to by each thread. We formalise our analysis within a novel abstract interpretation framework that is highly modular and can be easily extended to capture other structures for rely-guarantee conditions. We formalise two versions of our approach and evaluate their implementations on a simple programming language. |
| title | Generating Rely-Guarantee Conditions with the Conditional-Writes Domain |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.17142 |