一句话：提出基于归纳公理的可靠精化方法，弥合一阶抽象与良基/有限域语义间的鸿沟，消除伪状态。
一阶逻辑常用于堆操作程序、分布式协议等无界域系统的抽象建模，但其语义无法区分有限与无限结构，也无法定义良基关系，因而会产生伪状态与虚假行为，阻碍验证。论文针对抽象序关系，基于良基归纳分别形式化良基语义与有限域语义的可靠公理模式；利用必然无限的伪反模型指导公理实例化；并在 Ordered Self-Cycle（OSC）一阶逻辑片段中给出这两种语义到标准语义的可靠且完备归约，证明 OSC 下可满足性可判定。原型工具在分布式协议与堆程序例子中快速找到所需公理，完成验证并消除伪状态。
First-order logic has proved to be a versatile and expressive tool as the basis of abstract modeling languages. Used to verify complex systems with unbounded domains, such as heap-manipulating programs and distributed protocols, first-order logic, and specifically uninterpreted functions and quantifiers, strike a balance between expressiveness and amenity to automation. However, first-order logic semantics may differ in important ways from the intended semantics of the modeled system, due to the inability to distinguish between finite and infinite first-order structures, for example, or the undefinability of well-founded relations in first-order logic. This semantic gap may give rise to spurious states and unreal behaviors, which only exist as an artifact of the first-order abstraction and impede the verification process. In this paper we take a step towards bridging this semantic gap. We present an approach for soundly refining the first-order abstraction according to either well-founded semantics or finite-domain semantics, utilizing induction axioms for an abstract order relation, a common primitive in verification. We first formalize sound axiom schemata for each of the aforementioned semantics, based on well-founded induction. Second, we show how to use spurious counter-models, which are necessarily infinite, to guide the instantiation of these axiom schemata. Finally, we present a sound and complete reduction of well-founded semantics and finite-domain semantics to standard semantics in the recently discovered Ordered Self-Cycle (OSC) fragment of first-order logic, and prove that satisfiability under these semantics is decidable in OSC. We implement a prototype tool to evaluate our approach, and test it on various examples where spurious models arise, from the domains of distributed protocols and heap-manipulating programs. Our tool quickly finds the necessary axioms to refine the semantics, and successfully completes the verification process, eliminating the spurious system states that blocked progress.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{EladS25,
title = {Axe ’Em: Eliminating Spurious States with Induction Axioms},
author = {Neta Elad and Sharon Shoham},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704853}
}