Sound and Complete Invariant-Based Heap Encodings (Technical Report)

Zafer Esen, Philipp Rümmer, Tjark Weber

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 s…