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

TL;DR

This paper introduces a novel approach for finding infinite models in first-order logic formulas, aiding in debugging and verification by identifying models that existing solvers cannot find, especially in cases involving infinite structures.

Contribution

The paper presents symbolic structures for representing infinite models, an effective model finding procedure, and a new decidable fragment of first-order logic that guarantees the existence of such models.

Findings

Successfully finds infinite counter-models in verification problems

Outperforms SMT solvers like Z3, cvc5, and Vampire which diverge on these problems

Demonstrates applicability to distributed protocols and heap programs

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.