The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915819539136512 |
|---|---|
| author | Schüssele, Frank Zumkeller, Matthias Lagunes-Rochin, Miriam Klumpp, Dominik |
| author_facet | Schüssele, Frank Zumkeller, Matthias Lagunes-Rochin, Miriam Klumpp, Dominik |
| contents | Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact correctness proofs for concurrent programs is challenging, as the correctness arguments may depend on the particular interleaving, which can lead to exponential explosion. We present an approach that converts an interleaving-based correctness proof, as generated by many algorithmic verifiers, into a thread-modular correctness proof in the style of Owicki and Gries. We automatically synthesize ghost variables that capture the relevant interleaving information, and abstract away irrelevant details. Our evaluation shows that the approach is efficient in practice and generates compact proofs, compared to a baseline. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_20369 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version) Schüssele, Frank Zumkeller, Matthias Lagunes-Rochin, Miriam Klumpp, Dominik Programming Languages Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact correctness proofs for concurrent programs is challenging, as the correctness arguments may depend on the particular interleaving, which can lead to exponential explosion. We present an approach that converts an interleaving-based correctness proof, as generated by many algorithmic verifiers, into a thread-modular correctness proof in the style of Owicki and Gries. We automatically synthesize ghost variables that capture the relevant interleaving information, and abstract away irrelevant details. Our evaluation shows that the approach is efficient in practice and generates compact proofs, compared to a baseline. |
| title | The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version) |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2511.20369 |