Correctness Witness Validation by Abstract Interpretation
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915182477836288 |
|---|---|
| author | Saan, Simmo Schwarz, Michael Erhard, Julian Seidl, Helmut Tilscher, Sarah Vojdani, Vesal |
| author_facet | Saan, Simmo Schwarz, Michael Erhard, Julian Seidl, Helmut Tilscher, Sarah Vojdani, Vesal |
| contents | Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_16572 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Correctness Witness Validation by Abstract Interpretation Saan, Simmo Schwarz, Michael Erhard, Julian Seidl, Helmut Tilscher, Sarah Vojdani, Vesal Programming Languages Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own. |
| title | Correctness Witness Validation by Abstract Interpretation |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2310.16572 |