Researchers crack decades-old problem in program verification
A new technique automatically verifies that complex software won't crash or leak data when managing large, unpredictable data structures—a longstanding barrier to safer code. The breakthrough extends verification tools far beyond their current reach, potentially reducing costly bugs in production systems that rely on linked lists, trees, and other heap-based structures.
Originaltitel: Sound and Complete Invariant-Based Heap Encodings
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.