Axe 'Em: Eliminating Spurious States with Induction Axioms
Neta Elad, Sharon Shoham
TL;DR
This work addresses the gap between standard first-order logic semantics and the intended well-founded or finite-domain semantics when verifying unbounded systems. It introduces sound induction axiom schemata over a common order to refine abstractions and reduce satisfiability to the OSC fragment, enabling decidability results and automated refinement. The authors formalize WF and finite-domain axioms, develop a symbolic-model guided method to instantiate axioms from spurious counter-models, prove decidability in OSC-OSC, and implement a prototype tool that solves numerous Paxos and heap-verification examples. The approach enhances verification automation by systematically eliminating spurious states while maintaining soundness and completeness within OSC, with practical impact on distributed protocols and heap-manipulating programs.
Abstract
First-order logic (FOL) 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, FOL, and specifically uninterpreted functions and quantifiers, strike a balance between expressiveness and amenity to automation. However, FOL 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 FOL. 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 FOL, 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. Our tool quickly finds the necessary axioms to refine the semantics, and successfully completes the verification process.