Sound and Complete Invariant-Based Heap Encodings (Technical Report)
Abstract
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.
Cite
@article{arxiv.2504.15844,
title = {Sound and Complete Invariant-Based Heap Encodings (Technical Report)},
author = {Zafer Esen and Philipp Rümmer and Tjark Weber},
journal= {arXiv preprint arXiv:2504.15844},
year = {2026}
}
Comments
39 pages, 6 figures. To appear in Proceedings of the ACM on Programming Languages (PACMPL), Volume 10, Issue OOPSLA1, 2026. This version includes a 10-page appendix containing detailed proofs and extended experimental evaluation results