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求解器和定理证明器在此类问题上会发散。