Sound and Complete Invariant-Based Heap Encodings (Technical Report)
This work addresses the problem of verifying heap-manipulating programs for developers and verification tool users, offering a foundational advancement with sound and complete invariants.
The paper tackles the challenge of verifying programs with heap-allocated data structures by introducing time-indexed heap invariants, a novel encoding that reduces verification to integer programs, and demonstrates that it significantly extends the capability of existing tools, allowing automatic verification of previously unverifiable programs.
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.