Verification of SMT Systems with Quantifiers

We consider the problem of invariant checking for transition systems using SMT and quantified variables ranging over finite but unbounded domains. We propose a general approach, obtained by combining two ingredients: exploration of a finite instance, to obtain candidate inductive invariants, and instantiation-based techniques to discharge quantified queries. A thorough experimental evaluation on a wide range of benchmarks demonstrates the generality and effectiveness of our approach. Our algorithm is the first capable of approaching in a uniform way such a large variety of models.