PaperlayerView exact revision on arXiv

Source-linked AI summary

IC3 Modulo Theories via Implicit Predicate Abstraction

Alessandro Cimatti, Alberto Griggio, Sergio Mover, Stefano Tonetta

arXiv:1310.6847v1cs.LOcs.SE

TL;DR

Infinite-state IC3 extensions can require theory-specific reasoning that may be unavailable or inefficient. IC3+IA integrates IC3 with implicit predicate abstraction and incremental refinement, and experiments report effectiveness across a wide benchmark set and multiple theories.

  • Problem

    SMT-based IC3 extensions can rely on theory-specific techniques such as quantifier elimination that may be unavailable or inefficient.

    Source: §1 · p. 2

  • Method

    IC3+IA runs IC3 over abstraction predicates and uses implicit abstraction to avoid explicitly computing abstract transitions, refining the predicates for spurious counterexamples.

    Source: §1 · p. 2, §3.1 · p. 6, §3.3 · p. 8

  • Results

    Experiments on a wide benchmark set confirm IC3+IA’s generality across LRA, BV, and LIA and its effectiveness with large numbers of predicates.

    Source: §1 · p. 2, §6 · p. 15

  • Takeaways & Limitations

    The approach handles a wide range of background theories without ad-hoc extensions, provided an effective abstraction-refinement technique is available.

    Source: §1 · p. 2

    The predicate count can sometimes increase, and removing a predicate may harm later analysis if it becomes necessary.

    Source: Impact of number of predicates · p. 13

Abstract

from arXiv · show

We present a novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit (predicate) Abstraction, a technique that expresses abstract tran- sitions without computing explicitly the abstract system and is incremental with respect to the addition of predicates. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discov- ering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike current SMT gener- alizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available, and can moreover be inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improve- ment, as our experiments demonstrate.

1 Introduction

IC3’s finite-state success has motivated extensions to infinite-state systems, but existing SMT-based approaches often depend on theory-specific techniques that may be unavailable or inefficient. IC3+IA combines IC3 with implicit predicate abstraction, and experiments report broad theory coverage and strong performance.

1 Introduction

  • IC3 verifies invariant properties by over-approximating reachable states and generalizing clauses while disproving candidate counterexamples.For finite-state systems, it is implemented using Boolean SAT solvers.Source: §1 · p. 1
  • Existing IC3 Modulo Theories approaches may require quantifier elimination or theory-specific clause generalization, which can be unavailable or inefficient.These approaches reason over SMT descriptions of infinite-state transition systems.Source: §1 · pp. 1–2
  • IC3+IA combines IC3 with predicate abstraction and incrementally refines the abstraction when concrete simulation shows an abstract counterexample is spurious.IC3+IA generates clauses over the current abstraction predicates and uses implicit abstraction to express abstract transitions without computing the abstract system explicitly.Source: §1 · p. 2
  • Experiments report IC3+IA handles LRA, LIA, and fixed-size bit-vectors, and outperforms a wide range of verification tools on heterogeneous benchmarks.The compared tools include bit-level IC3, other IC3 Modulo Theories approaches, k-induction, and invariant discovery.Source: §1 · p. 2

2 Background

The section introduces transition systems and IC3, then explains predicate abstraction as a way to reduce the search space while preserving invariant-checking conclusions. It also outlines how implicit abstraction encodes abstract paths without explicitly computing the abstract system.

2.1 Transition Systems

  • A transition system specifies state variables, initial states, and transitions; verification checks that every state along every path satisfies the property.An inductive invariant contains the initial states and is preserved by every transition.Source: §2.1 · p. 3

2.2 IC3 with SMT

  • IC3 builds a trace of progressively stronger frames, blocking bad states with relative-inductive clauses and propagating clauses until a fixpoint yields an inductive invariant.Blocking may recursively generate earlier predecessor states to block; propagation reaches a fixpoint when consecutive frames are identical.Source: §2.2 · p. 4
  • Earlier SMT extensions of IC3 require theory-specific handling of counterexamples, including existential elimination or theory-aware generalization.In the described approach, a Boolean SAT model can supply a predecessor cube, but first-order theory atoms may couple primed and unprimed variables.Source: §2.2 · pp. 4–5

Predicate abstraction

  • Predicate abstraction represents states with predicates and abstracts initial and transition formulas; implicit abstraction encodes abstract paths without explicitly computing the abstract system.The path encoding links disconnected concrete transitions by requiring each gap to lie in the same abstract state.Source: Predicate abstraction · p. 5
  • Explicit predicate abstraction requires eliminating existential quantifiers, which may create a bottleneck for model checkers that handle only quantifier-free formulas.Some techniques instead compute weaker, more abstract systems.Source: Predicate abstraction · p. 5

3 IC3 with Implicit Abstraction

IC3+IA runs IC3 over an abstract state space defined by predicates, using implicit abstraction to avoid explicitly computing abstract transitions. It simulates abstract counterexamples concretely, refines spurious ones by adding predicates, and preserves prior clauses during refinement.

3.1 Main idea

  • IC3+IA mimics IC3 over the state space defined by predicates, using implicit abstraction to avoid explicitly computing the abstract transition relation.Its abstract relative-induction check corresponds to the abstract check, and the theorem relates their satisfiability.Source: §3.1 · p. 6

3.2 The algorithm

  • The algorithm replaces concrete states with P-cubes, uses AbsRelInd instead of RelInd, and adds predicates when an abstract counterexample is spurious.Blocking recursively strengthens frames or produces an abstract counterexample; propagation moves inductive P-clauses forward between frames.Source: §3.2 · pp. 6–7, Figure 2 · p. 7

3.3 Simulation and refinement

  • Abstract counterexamples are simulated on the concrete system; a satisfiable bounded-path formula witnesses a real violation, while a spurious counterexample triggers refinement.The refinement procedure need only eliminate the spurious counterexamples and can use interpolation, unsat-core extraction, or weakest preconditions.Source: §3.3 · pp. 7–8
  • Refinement only adds predicates, strengthening the abstract transition relation and allowing IC3+IA to retain all clauses in its frames.This makes refinement fully incremental rather than requiring clauses from the previous search to be discarded.Source: §3.3 · p. 8

3.4 Correctness

  • IC3+IA is sound: a true result proves the concrete safety property, while a false result follows a concrete counterexample simulation.Its relative-completeness result applies once the predicate set abstracts the system so that the abstract system satisfies the property.Source: §3.4 · p. 9
  • The correctness argument establishes that an abstract counterexample is a path violating the abstract property, and that a fixed-point frame supplies an inductive invariant.The frame invariants include initialization, progression, relative induction, and preservation of the property.Source: §3.4 · pp. 8–9

4 Related Work

The paper situates IC3+IA at the intersection of predicate abstraction and IC3, contrasting its implicit abstraction approach with prior theory-specific and Boolean-only extensions.

4 Related Work

  • IC3+IA is presented as the first integration of implicit abstraction in a CEGAR loop, using it with IC3 to avoid theory-specific generalization.Implicit abstraction had previously been used with k-induction to avoid explicitly computing the abstract system.Source: §4 · p. 9
  • A prior lazy-abstraction approach is limited to Boolean systems and uses visible-variable abstraction rather than predicate abstraction.It also uses a modified concrete version of IC3 for refinement.Source: §4 · pp. 9–10
  • Earlier SMT extensions of IC3 for linear real arithmetic rely on theory-specific procedures, while IC3+IA targets a broader class of systems without such procedures.The cited approaches include quantifier elimination and interpolant-based generalization; the latter does not exploit relative induction.Source: §4 · p. 10
  • The paper contrasts IC3+IA with a timed-automata approach and an ad-hoc bit-vector extension, noting its broader applicability and non-bit-vector-specific design.The timed-automata method exploits finite region-graph partitioning; the bit-vector extension may handle some operators inefficiently.Source: §4 · p. 10

5 Experimental Evaluation

The experiments compare implicit-abstraction IC3 variants with other verification tools across LRA, timed-automata, bit-vector, and LIA benchmarks. They report performance benefits on LRA and timed-automata tests, tolerance for many predicates, and results extending to BV and LIA.

5.1 Performance Benefits of Implicit Abstraction

  • IC3+IA(LRA) solved 20 more instances than IC3(LRA), was more than one order of magnitude faster in many cases, and no instance solved by IC3(LRA) was missed.Both abstraction-based variants outperformed the other compared algorithms, including Z3; the explicit predicate-abstraction CEGAR configuration solved only 10 instances.Source: §5.1 · pp. 11–12, Figure 3 · p. 11
  • 100 instances in 772 seconds for IC3+IA(LRA), versus 41 in 3953 seconds for ATMOC, on a preliminary timed-automata comparison.The comparison used a randomly selected subset of nontrivial ATMOC properties and was described as preliminary.Source: §5.1 · p. 12, Figure 4 · p. 12

Impact of number of predicates

  • Predicate reduction usually lowered the predicate count but had little effect on execution time, and both IC3+IA(LRA) versions solved the same number of problems.IC3+IA(LRA) handled up to 800 predicates and solved most safe instances with more than 100, unlike explicit abstraction techniques that can blow up with a few dozen.Source: Impact of number of predicates · p. 13, Figure 5 · p. 13

5.2 Expressiveness Benefits of Implicit Abstraction

  • The second experimental analysis evaluates Implicit Abstraction for applying IC3 to systems unsupported by methods of, instantiating IC3+IA(T) and TREEIC3+IA(T) over Linear Integer Arithmetic (LIA) and fixed-size bit-vectors (BV).The BV evaluation used over 200 benchmark instances from software verification.Source: §5.2 · p. 14, IC3 for BV · p. 14

IC3 for BV

  • On software-verification BV benchmarks, IC3+IA(BV) and TREEIC3+IA(BV) outperformed bit-level IC3 implementations, with TREEIC3+IA(BV) slightly better despite solving the same number of instances.Figure 6 reports these results.Source: IC3 for BV · p. 14, Figure 6 · p. 14

IC3 for LIA

6 Conclusion

IC3+IA extends IC3 to infinite-state transition systems using implicit predicate abstraction, with incremental refinement that preserves previously found clauses. Experiments support its generality across LRA, BV, and LIA and its effectiveness on a wide benchmark set.

6 Conclusion

  • IC3+IA applies IC3 to infinite-state transition systems by extending it with implicit predicate abstraction.Its distinguishing feature is that counterexamples to induction and relative inductive clauses use abstraction predicates.Source: §6 · p. 15
  • Incremental refinement lets the procedure retain clauses found in previous iterations as it adds predicates.Source: §6 · p. 15
  • Experiments on a wide benchmark set support IC3+IA’s generality across LRA, BV, and LIA and its effectiveness with large numbers of predicates.The results also include comparisons against dedicated verification engines.Source: §6 · p. 15
  • The authors identify arrays, non-linear arithmetic, other predicate-discovery methods, and liveness properties as directions for future work.Source: §6 · p. 16

Related papers

Loading 1310.6847v1…