A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)

TL;DR

The paper tackles termination concerns in E-matching-based axiomatisations for SMT-based verification by introducing a solver-agnostic, small-step operational semantics that models enabling matches and learned facts through an E-interface $E^{I}$ and an E-history $E^{H}$. A match judgement governs which instantiations are allowed, and transitions include split, bot, sat, and inst; the authors then develop a termination framework that classifies axioms as non-generative, generative, or nested and defines a progress measure $M(s) = (\Sigma(s), \Theta(s))$ that decreases lexicographically along traces. They apply this to a comprehensive set-theory axiomatisation adapted from Dafny and Viper, proving instantiation termination and outlining a methodology for constructing invariants and over-approximations to bound enabled matches. The work enables terminating responses to ground theory queries and provides a foundation for future work on completeness and theory solvers.

Abstract

SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to be challenging. If quantifier instantiation is not carefully controlled, then runtime and outcomes can be brittle and hard to predict. In particular, uncontrolled quantifier instantiation can lead to unexpected incompleteness and even non-termination. E-matching is the most widely-used approach for controlling quantifier instantiation, but when axiomatisations are complex, even experts cannot tell if their use of E-matching guarantees completeness or termination. This paper presents a new formal model that facilitates the proof, once and for all, that giving a complex E-matching-based axiomatisation to an SMT solver, such as Z3 or cvc5, will not cause non-termination. Key to our technique is an operational semantics for solver behaviour that models how the E-matching rules common to most solvers are used to determine when quantifier instantiations are enabled, but abstracts over irrelevant details of individual solvers. We demonstrate the effectiveness of our technique by presenting a termination proof for a set theory axiomatisation adapted from those used in the Dafny and Viper verifiers.