一句话：提出 FO-完全性标准，并给出首个支持隐式 heaplet、可 FO-完全验证的 frame logic 与 separation logic 及 SMT 验证方法。
针对表达力强的堆逻辑程序验证本质上不完备的问题，论文提出将算法技术置于 FO-完全性这一更稳健的完备性标准之下：若递归定义按 fixpoint（而非 least fixpoint）解释时定理有效，系统最终应能证明。作者总结设计此类逻辑的原则，并给出首批具有隐式 heaplet 且可 FO-完全验证的堆逻辑：frame logic (FL) 与受 FL 语义启发的 separation logic (SL-FL)。他们提出一种适合 FO-完全推理的验证条件生成技术，通过量词实例化与 SMT 求解器实现。原型工具在数据结构操作基准上展示了逻辑表达力与验证效果。
Program verification techniques for expressive heap logics are inevitably incomplete. In this work we argue that algorithmic techniques for reasoning with expressive heap logics can be held up to a different robust theoretical standard for completeness: FO-Completeness. FO-completeness is a theoretical guarantee that all theorems that are valid when recursive definitions are interpreted as fixpoint definitions (instead of least fixpoint) are guaranteed to be eventually proven by the system. We illustrate a set of principles to design such logics and develop the first two heap logics that have implicit heaplets and that admit FO-Complete program verification. The logics we develop are a frame logic (FL) and a separation logic (SL-FL) that has an alternate semantics inspired by frame logic. We show a verification condition generation technique that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We implement tools that realize our technique and show the expressiveness of our logics and the efficacy of the verification technique on a suite of benchmarks that manipulate data structures.
@article{paperbot3199,
title = {FO-Complete Program Verification for Heap Logics},
author = {Adithya Murali and Hrishikesh Balakrishnan and Aaron Councilman and P. Madhusudan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720447}
}