An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification

TL;DR

The paper tackles the challenge of quantifiers in first-order logic for deductive verification, where many formulas admit only infinite counter-models that SMT solvers fail to detect. It introduces symbolic structures, a finite representation of certain infinite models, and a symbolic-search procedure that reduces model checking to Linear Integer Arithmetic (LIA), enabling efficient discovery of infinite counter-models. It then defines a new decidable fragment, Ordered Self Cycle (OSC), which extends the Bernays–Schönfinkel–Ramsey (EPR) class by permitting a linear order on an infinite sort and a limited cyclicity, proving a small symbolic model property and turning satisfiability into a finite search over templates. The authors implement FEST (Find and Evaluate Symbolic structures via Templates) and demonstrate it on 21 cases from distributed protocols and heap-based programs, where FEST finds infinite counter-models that elude Z3, cvc5, and Vampire, offering actionable feedback to refine modeling and axioms. These results provide a practical pathway to diagnosing verification gaps and guiding the formulation of induction or axioms to achieve verification success. All mathematical constructs are presented with a formal grounding in $\mathsf{FOL}$, $\mathsf{LIA}$, OSC, and template-based satisfiability, with broad potential impact on SMT-based verification workflows.

Abstract

First-order logic, and quantifiers in particular, are widely used in deductive verification. Quantifiers are essential for describing systems with unbounded domains, but prove difficult for automated solvers. Significant effort has been dedicated to finding quantifier instantiations that establish unsatisfiability, thus ensuring validity of a system's verification conditions. However, in many cases the formulas are satisfiable: this is often the case in intermediate steps of the verification process. For such cases, existing tools are limited to finding finite models as counterexamples. Yet, some quantified formulas are satisfiable but only have infinite models. Such infinite counter-models are especially typical when first-order logic is used to approximate inductive definitions such as linked lists or the natural numbers. The inability of solvers to find infinite models makes them diverge in these cases. In this paper, we tackle the problem of finding such infinite models. These models allow the user to identify and fix bugs in the modeling of the system and its properties. Our approach consists of three parts. First, we introduce symbolic structures as a way to represent certain infinite models. Second, we describe an effective model finding procedure that symbolically explores a given family of symbolic structures. Finally, we identify a new decidable fragment of first-order logic that extends and subsumes the many-sorted variant of EPR, where satisfiable formulas always have a model representable by a symbolic structure within a known family. We evaluate our approach on examples from the domains of distributed consensus protocols and of heap-manipulating programs. Our implementation quickly finds infinite counter-models that demonstrate the source of verification failures in a simple way, while SMT solvers and theorem provers such as Z3, cvc5, and Vampire diverge.

Figures (10)

• Figure 1: The Echo Machine in pseudo-Ivy.
• Figure 2: A CTI for echo_start. Values are depicted as squares and rounds as circles.
• Figure 3: Model-checking symbolic structure $S$ and assignment $v$ by translation to LIA.
• Figure 4: The heuristic template family ${\mathbb{H}}$, parameterized by domain ${\mathcal{D}}$.
• Figure 5: Explication of a symbolic structure constructed as in \ref{['sec:single-sort-construction']}. Each circle depicts an element. The labels $S_i, G_i$ denote different sets of atoms which correspond to different nodes in the symbolic structure. I.e., each $S_i$ and $G_j$ is a unique set of element atoms \ref{['enum:domain:element']}, image atoms \ref{['enum:domain:image']}, and mixed atoms \ref{['enum:domain:mixed']}. The sets $G_1, G_2, \dots$ include at least one atom of the form $x \mathrel{{\approx}} g$, where $g$ is some ground term, thus refer to regular nodes. The sets $S_1, S_2, \dots$ do not include any atom of the form $x \mathrel{{\approx}} g$, thus refer to summary nodes. The arrows between the elements depict $\mathrel{\prec}^{{\mathcal{E}}{\left( S \right)}}$ by denoting immediate successors. Note that the order between the explicit elements of, for example, $S_4, S_5$ and $S_6$ follows a fixed pattern.

Theorems & Definitions (24)

• Remark 1
• definition 1
• definition 2
• theorem 2
• definition 3
• definition 4
• theorem 3
• theorem 4
• corollary 1
• lemma 1