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

TL;DR

This paper introduces a formal model that proves the termination of E-matching-based axiomatisations in SMT solvers, enhancing reliability in program analysis involving quantifiers.

Contribution

It provides a new formal framework and operational semantics to guarantee termination of complex E-matching axiomatisations in SMT solvers.

Findings

Proves termination for a set theory axiomatisation used in Dafny and Viper.

Models solver behavior to predict quantifier instantiation outcomes.

Ensures completeness and termination in SMT-based reasoning with complex axioms.

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.