Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints

Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not even admit complete procedures, let alone decidable ones. In this paper, we undertake a novel approach for synthesizing inductive hypotheses in order to prove validity in this logic. The key techniques rely on utilizing several kinds of finite first-order models as counterexamples that capture non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs, demonstrating the effectiveness of our methodology.