Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (extended version)

TL;DR

This paper introduces a novel technique to identify and remedy overly restrictive matching patterns in SMT-based program verifiers, improving proof completeness and soundness by synthesizing missing triggering terms.

Contribution

It presents the first algorithm for synthesizing missing triggering terms to address overly restrictive matching patterns in SMT-based verifiers.

Findings

The technique helps detect verification errors caused by restrictive patterns.

It enables refinement of matching patterns to improve proof success.

The method can identify potential unsoundness due to axiomatization issues.

Abstract

Universal quantifiers occur frequently in proof obligations produced by program verifiers, for instance, to axiomatize uninterpreted functions and to express properties of arrays. SMT-based verifiers typically reason about them via E-matching, an SMT algorithm that requires syntactic matching patterns to guide the quantifier instantiations. Devising good matching patterns is challenging. In particular, overly restrictive patterns may lead to spurious verification errors if the quantifiers needed for a proof are not instantiated; they may also conceal unsoundness caused by inconsistent axiomatizations. In this paper, we present the first technique that identifies and helps the users remedy the effects of overly restrictive matching patterns. We designed a novel algorithm to synthesize missing triggering terms required to complete a proof. Tool developers can use this information to refine their matching patterns and prevent similar verification errors, or to fix a detected unsoundness.