Invariant Checking for SMT-based Systems with Quantifiers
CoRR(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要