FO-Complete Program Verification for Heap Logics

TL;DR

This work tackles the challenge of complete automatic verification for expressive heap logics by introducing two FO-complete logics: Frame Logic (FL) and a frame-logic-inspired Separation Logic (SL-FL) with implicit heaplets. It develops a verification pipeline that uses a cloud operator to eliminate quantifiers, translates SL-FL into FL, and relies on FO-complete reasoning (via natural proofs) over a one-way fragment of first-order logic, FORD, to discharge verification conditions. The authors implement toolchains, FLV and SLFLV, and demonstrate through a 29-program benchmark suite that these logics can express rich data-structure specifications and verify them efficiently, with SL-FL showing expressiveness at some performance cost. The results establish a practical, theoretically grounded standard of FO-completeness for heap logics, paving the way for more robust, predictable automated verification in memory-managed settings and suggesting avenues for automated lemma synthesis and broader toolchains.

Abstract

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.

Figures (11)

• Figure 1: Frame Logic with guarded quantification. $\mathit{Var}_\mathit{Loc}$ denotes variables over the foreground sort and $\mathit{Set}(\mathit{Loc})$ denotes the sort consisting of sets of foreground elements. Terms and formulas are assumed to be well-typed for simplicity of presentation.
• Figure 2: Semantics of Support operator. $\llbracket \!e\! \rrbracket_M$ refers to the interpretation of an expression $e$ in a model $M$. The support is defined as the least interpretation satisfying the given equations.
• Figure 3: The syntax of the programming language. Here, $x,y$ are location variables of type $Loc$, $c$ is a location constant, $f$ is a pointer of type $Loc \rightarrow Loc$, $d$ is a data field of type $Loc \rightarrow \tau_{\text{bs}}$ for some background sort $\tau_\text{bs}$, $be$ is a background expression, $v$ is a variable of a background sort, $\eta$ is a boolean expression without any dereferences. Finally, $g$ is a function of type $\tau_{1}\times\dots\times\tau_{m} \rightarrow \tau^{\prime}_{1}\times\dots\times\tau^{\prime}_{n}$ for some $m,n$ where $\tau_{i}, \tau^{\prime}_{i} \in \mathcal{S}$. This is a method whose body is itself a program whose variables are a superset of the input variables $p_{i}$ of type $\tau_{i}$ and the output variables $q_{j}$ of type $\tau^{\prime}_{j}$.
• Figure 4: Base Separation Logics with FL inspired semantics $\textit{SL-FL}_b$ and $\textit{SL-FL}_b^\vee$; H.I.:"heap-independent"
• Figure 5: Definition of supports and semantics for base separation logic $\textit{SL-FL}_b$, mutually defined. Definitions for $\textit{SL-FL}_b^\vee$ include the rules for disjunction. Set operations on supports that evaluate to $\bot$ evaluate to $\bot$.

Theorems & Definitions (14)

• theorem 1: Trakhtenbrot's Theorem
• proposition 1
• theorem 2: Proof in Appendix \ref{['app:sourcesofinc']}
• theorem 3: Non-Unique Heaplets make SL Incomplete
• definition 1: Hoare Triple Validity
• lemma 1
• lemma 2
• lemma 3
• lemma 4: Eliminating Quantification using the Cloud Operator
• definition 2