Quantifiers on Demand

TL;DR

The paper introduces Quic3, a novel algorithm extending IC3 for inferring universally quantified invariants over combined LIA and Arrays theories, improving automated program verification.

Contribution

Quic3 is a new algorithm that manages quantified generalization and instantiation, enabling progress in verifying array-manipulating programs with complex theories.

Findings

Implemented Quic3 in Z3 solver.

Successfully verified array-manipulating C programs.

Made progress by exploring longer executions despite non-guaranteed convergence.

Abstract

Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theory of Arrays, further complicates the problem by requiring inference and reasoning with universally quantified formulas. In this paper, we present a new algorithm, Quic3, that extends IC3 to infer universally quantified invariants over the combined theory of LIA and Arrays. Unlike other approaches that use either IC3 or an SMT solver as a black box, Quic3 carefully manages quantified generalization (to construct quantified invariants) and quantifier instantiation (to detect convergence in the presence of quantifiers). While Quic3 is not guaranteed to converge, it is guaranteed to make progress by exploring longer and longer executions. We have implemented Quic3 within the Constrained Horn Clause solver engine of Z3 and experimented with it by applying Quic3 to verifying a variety of public benchmarks of array manipulating C programs.