A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)
CoRR(2024)
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.
MoreTranslated text
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined