Invariant Checking for SMT-Based Systems with Quantifiers

This article addresses the problem of checking invariant properties for a large class of symbolic transition systems defined by a combination of SMT theories and quantifiers. State variables can be functions from an uninterpreted sort (finite but unbounded) to an interpreted sort, such as the integers under the theory of linear arithmetic. This formalism is very expressive and can be used for modeling parameterized systems, array-manipulating programs, and more. We propose two algorithms for finding universal inductive invariants for such systems. The first algorithm combines an IC3-style loop with a form of implicit predicate abstraction to construct an invariant in an incremental manner. The second algorithm constructs an under-approximation of the original problem and searches for a formula which is an inductive invariant for this case; then, the invariant is generalized to the original case and checked with a portfolio of techniques. We have implemented the two algorithms and conducted an extensive experimental evaluation, considering various benchmarks and different tools from the literature. As far as we know, our method is the first capable of handling in a large class of systems in a uniform way. The experiment shows that both algorithms are competitive with the state of the art.