Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Invariant Checking for SMT-based Systems with Quantifiers

Gianluca Redondi, Alessandro Cimatti, Alberto Griggio, Kenneth McMillan

TL;DR

The paper tackles invariant checking for SMT-based systems with quantifiers by introducing two automated approaches. UPDR with implicit abstraction (Updria) extends IC3/PDR to synthesize universally quantified invariants under SMT theories, at the cost of heavy quantified reasoning. The second method (Lambda) relies on grounding a finite index domain, generalizing invariants from small ground instances, and lifting them to the full system via abstraction or SMT-based checks; this approach trades some completeness for practicality. Extensive experiments across diverse benchmarks show both methods are general and competitive with existing tools, with complementary strengths depending on theory and quantifier structure. The work advances uniform handling of large classes of parametrized and array-based systems and sets the stage for future work on quantifier alternation and liveness properties.

Abstract

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.

Invariant Checking for SMT-based Systems with Quantifiers

TL;DR

The paper tackles invariant checking for SMT-based systems with quantifiers by introducing two automated approaches. UPDR with implicit abstraction (Updria) extends IC3/PDR to synthesize universally quantified invariants under SMT theories, at the cost of heavy quantified reasoning. The second method (Lambda) relies on grounding a finite index domain, generalizing invariants from small ground instances, and lifting them to the full system via abstraction or SMT-based checks; this approach trades some completeness for practicality. Extensive experiments across diverse benchmarks show both methods are general and competitive with existing tools, with complementary strengths depending on theory and quantifier structure. The work advances uniform handling of large classes of parametrized and array-based systems and sets the stage for future work on quantifier alternation and liveness properties.

Abstract

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.
Paper Structure (41 sections, 29 theorems, 39 equations, 7 figures, 3 tables, 3 algorithms)

This paper contains 41 sections, 29 theorems, 39 equations, 7 figures, 3 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Preliminaries
  4. Symbolic transition systems
  5. Approximate Reachability Sequence
  6. Abstraction and Refinement
  7. Refinement by Craig interpolants
  8. Problem statement
  9. Array-based transition systems
  10. The invariant problem for array-based transition systems
  11. Ground instances
  12. UPDR with implicit abstraction
  13. Overview
  14. Implicit Indexed Predicate Abstraction
  15. Algorithm description and pseudocode
  16. ...and 26 more sections

Key Result

Proposition 1

Let $C = ( X,\iota(X), \tau(X, X'))$ be a transition system and $\phi$ a formula. Let $F_0, \dots, F_N$ be an approximate reachability sequence for $C$ and $\phi$. If for some $0 \leq i < N, F_{i+1} \models F_i$, then $C \models \phi$. Moreover, $F_i$ is an inductive invariant for $\phi$ and $C$.

Figures (7)

  • Figure 1: An overview of the algorithm.
  • Figure 2: Plot comparing different options of Lambda
  • Figure 3: Plot comparing different options of Updria
  • Figure 4: Scatter plot comparing Updria and Lambda
  • Figure 5: Plot for Mcmt family
  • ...and 2 more figures

Theorems & Definitions (62)

  • Definition 1
  • Definition 2
  • Proposition 1: ic3
  • Definition 3: Simulation
  • Definition 4: Stuttering Simulation
  • Definition 5
  • Definition 6
  • Example 1
  • Proposition 2
  • Example 2
  • ...and 52 more