Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion

TL;DR

This paper introduces a novel algorithm for finding inductive invariants with quantifier alternations, improving scalability and effectiveness in complex distributed protocol verification by combining a breadth-first search and a new syntactic form.

Contribution

The paper presents a new PDR/IC3 algorithm that efficiently searches for inductive invariants with quantifier alternations using a combined breadth-first strategy and a specialized syntactic form.

Findings

Successfully solves more complex distributed protocol examples than existing methods.

Demonstrates improved scalability and effectiveness on a benchmark suite.

Introduces a syntactic form that manages the search space for quantified invariants.

Abstract

We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new syntactic form for quantifier-free bodies. The breadth-first strategy prevents inductive generalization from getting stuck in regions of the search space that are expensive to search and focuses instead on lemmas that are easy to discover. The new syntactic form is well-suited to lemmas with quantifier alternations by allowing both limited conjunction and disjunction in the quantifier-free body, while carefully controlling the size of the search space. Combining the breadth-first strategy with the new syntactic form results in useful inductive bias by prioritizing lemmas according to: (i) well-defined syntactic metrics for simple quantifier structures and quantifier-free bodies, and (ii) the empirically useful heuristic of preferring lemmas that are fast to discover. On a benchmark suite of primarily distributed protocols and complex Paxos variants, we demonstrate that our algorithm can solve more of the most complicated examples than state-of-the-art techniques.