This paper 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 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.

翻译：本文研究了由SMT理论与量词组合定义的一大类符号迁移系统的不变性属性检查问题。状态变量可以是未解释类型（有限但无界）到解释类型（如线性算术理论下的整数）的函数。该形式化表达具有高度表达能力，可用于建模参数化系统、数组操作程序等场景。我们提出两种算法来寻找此类系统的通用归纳不变量。第一种算法将IC3风格循环与隐式谓词抽象相结合，以增量方式构建不变量。第二种算法构建原始问题的下近似，搜索该场景下的归纳不变量公式；随后将不变量泛化至原始场景，并采用技术组合进行验证。我们实现了这两种算法并进行了广泛的实验评估，考虑了文献中的多种基准测试与不同工具。据我们所知，本方法是首个能够统一处理大规模系统类的方法。实验表明，两种算法均具备与前沿技术竞争的能力。