一句话：提出时间索引堆不变式，借助未解释谓词与预言变量将堆程序验证归约为整数程序验证，并首次同时实现可靠性与完备性。
堆分配数据结构（如链表、树）的规模可能无界，给程序验证带来巨大挑战。本文提出时间索引堆不变式（time-indexed heap invariants），一种新的基于不变式的堆编码方法：利用未解释谓词（uninterpreted predicates）与预言变量（prophecy variables），将堆操作程序的验证归约为仅含整数的程序验证。该编码通用且不依赖于具体数据结构。作者给出了形式化证明，论证编码的可靠性（soundness）与完备性（completeness），据称是首个同时具备这两点的基于堆不变式的方法。实验评估表明，时间索引堆不变式显著扩展了现有验证工具的能力，能够自动验证此前最先进工具无法处理的堆程序。
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.
@article{paperbot3806,
title = {Sound and Complete Invariant-Based Heap Encodings},
author = {Zafer Esen and Philipp Rümmer and Tjark Weber},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798228}
}