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.

翻译：一阶逻辑（特别是量词）广泛应用于演绎验证。量词对于描述具有无界域的系统至关重要，但给自动化求解器带来了困难。大量研究致力于寻找能证明不可满足性的量词实例化，从而确保系统验证条件的有效性。然而，在许多情况下公式是可满足的——这在验证过程的中间步骤中尤为常见。针对此类情况，现有工具仅能寻找有限模型作为反例。但部分量化公式虽可满足却仅有无限模型。当一阶逻辑被用于逼近归纳定义（如链表或自然数）时，此类无限反模型尤为典型。求解器无法发现无限模型导致这些情况下出现发散。本文致力于解决此类无限模型的寻找问题。这些模型能使使用者识别并修复系统建模及其属性中的缺陷。我们的方法包含三部分：首先，引入符号结构作为表示特定无限模型的手段；其次，描述一种有效模型寻找过程，该过程能符号化地探索给定符号结构族；最后，我们识别出一阶逻辑的新可判定片段，该片段扩展并涵盖了EPR的多排序变体，其中可满足公式总能在已知符号结构族内找到可表示的模型。我们在分布式共识协议和堆操作程序两个领域的实例上评估了该方法。我们的实现能快速发现无限反模型，以简洁方式揭示验证失败的根源，而Z3、cvc5和Vampire等SMT求解器及定理证明器则出现发散。