IC3

Kind 2 supports two SMT-based extensions of the SAT-based verification technique IC3. The challenge when lifting IC3 to infinite state systems is the computation of pre-images of the system’s transition relation. The first extension, IC3QE, uses quantifier elimination to compute the pre-image. If the input problem is in linear integer arithmetic, Kind 2 uses a built-in method that performs a fast approximate quantifier elimination. Otherwise, the quantifier elimination is delegated to an SMT solver, which is at this time possible with Z3 and cvc5.

The second extension, IC3IA, implements a version of IC3 that relies on implicit (predicate) abstraction by Cimatti et al. The main idea of the method is to work on an abstraction of the state space induced by a set of predicates so that the computation of pre-images of the system’s transition relation does not require the use of quantifier elimination. As with most abstraction methods, this introduces the problem of having to handle spurious abstract counterexamples for the property to be proven, that is, traces that falsify the property in the abstracted system but are not actual executions of the original system. The method addresses this problem by using an abstraction refinement technique based on logical interpolants. Kind 2 currently supports two proof-based interpolating SMT solvers for the generation of interpolants: MathSAT, SMTInterpol, and OpenSMT. In addition, Kind 2 also implements a built-in method for producing interpolants based on quantifier elimination that can be used with Z3 and cvc5. When the IC3IA engine is enabled, each property is handled separately by a different process; two when the built-in method for producing interpolants is used, one generating backward interpolants and another one generating forward interpolants.

To enable nothing but the IC3 engines (IC3QE and IC3IA), run

kind2 --enable IC3 <file>

If you only want to enable of the engines, e.g. IC3QE, run

kind2 --enable IC3QE <file>

IC3-IA Options

--smt_itp_solver {MathSAT | SMTInterpol | Z3qe | cvc5qe | OpenSMT} – set the SMT solver used for interpolation.

--ic3ia_max <int> – set the maximum number of IC3IA parallel processes. Each process checks an individual property.

IC3-QE Options

--qe_method {precise|impl|cooper} (default cooper) – select the quantifier elimination strategy: cooper for the built-in approximate method, precise or impl to delegate to the SMT solver. The precise strategy computes the exact pre-image, which is an expensive operation. The impl strategy under-approximates the result by computing a conjunctive implicant first. If the problem is not in linear integer arithmetic, cooper falls back to impl.

--smt_qe_solver {Z3 | cvc5} (default detect) – set the SMT solver used for quantifier elimination

To see other advanced options run --help_of ic3qe.