We develop the first two heap logics that have implicit heaplets and that admit FO-complete program verification. The notion of 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. The logics we develop are a frame logic ($\textit{FL}$) and a separation logic ($\textit{SL-FL}$) that has an alternate semantics inspired by frame logic. We show verification condition generation for FL that is amenable to FO-complete reasoning using quantifier instantiation and SMT solvers. We show $\textit{SL-FL}$ can be translated to FL in order to obtain FO-complete reasoning. 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.

翻译：我们开发了首个两种具有隐式堆片段且支持FO完全程序验证的堆逻辑。FO完全性这一概念提供了理论保证：当递归定义被解释为不动点定义（而非最小不动点）时，所有有效的定理都能确保最终被系统证明。我们开发的逻辑包括框架逻辑（$\textit{FL}$）和一种受框架逻辑启发而具有替代语义的分离逻辑（$\textit{SL-FL}$）。我们展示了适用于FO完全推理的FL验证条件生成方法，该方法可利用量词实例化与SMT求解器实现。我们证明$\textit{SL-FL}$可通过转换为FL来获得FO完全推理能力。我们实现了体现该技术的工具，并通过一系列操作数据结构的基准测试，展示了所提出逻辑的表达能力及验证技术的有效性。