Sound and Complete Invariant-Based Heap Encodings (Technical Report)
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_ | 1866915858061721600 |
|---|---|
| author | Esen, Zafer Rümmer, Philipp Weber, Tjark |
| author_facet | Esen, Zafer Rümmer, Philipp Weber, Tjark |
| contents | Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data structures. We present time-indexed heap invariants, a novel invariant-based heap encoding leveraging uninterpreted predicates and prophecy variables to reduce verification of heap-manipulating programs to verification of programs over integers only. Our encoding of heap is general and agnostic to specific data structures. To the best of our knowledge, our approach is the first heap invariant-based method that achieves both soundness and completeness. We provide formal proofs establishing the correctness of our encodings. Through an experimental evaluation, we demonstrate that time-indexed heap invariants significantly extend the capability of existing verification tools, allowing automatic verification of programs with heap that were previously out of reach for state-of-the-art tools. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_15844 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Sound and Complete Invariant-Based Heap Encodings (Technical Report) Esen, Zafer Rümmer, Philipp Weber, Tjark Logic in Computer Science F.3.1; D.2.4 Verification of programs operating on heap-allocated data structures, for instance lists or trees, poses significant challenges due to the potentially unbounded size of such data structures. We present time-indexed heap invariants, a novel invariant-based heap encoding leveraging uninterpreted predicates and prophecy variables to reduce verification of heap-manipulating programs to verification of programs over integers only. Our encoding of heap is general and agnostic to specific data structures. To the best of our knowledge, our approach is the first heap invariant-based method that achieves both soundness and completeness. We provide formal proofs establishing the correctness of our encodings. Through an experimental evaluation, we demonstrate that time-indexed heap invariants significantly extend the capability of existing verification tools, allowing automatic verification of programs with heap that were previously out of reach for state-of-the-art tools. |
| title | Sound and Complete Invariant-Based Heap Encodings (Technical Report) |
| topic | Logic in Computer Science F.3.1; D.2.4 |
| url | https://arxiv.org/abs/2504.15844 |