FO-Complete Program Verification for Heap Logics

TL;DR

This paper introduces two heap logics, FL and SL-FL, that enable FO-complete program verification for heap-manipulating programs, ensuring all valid recursive properties can be eventually proven.

Contribution

The paper presents the first FO-complete heap logics with implicit heaplets, enabling comprehensive verification of recursive heap properties.

Findings

Verification condition generation for FL is compatible with FO-complete reasoning.

SL-FL can be translated into FL for FO-complete reasoning.

Tools demonstrate the effectiveness and expressiveness on benchmark data structures.

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.