IC3

IC3/PDR is a recent technique by Aaron Bradley. IC3 alone can falsify and prove properties. To enable nothing but IC3, run

kind2 --enable IC3 <file>

The challenge when lifting IC3 to infinite state systems is the pre-image computation. If the input problem is in linear integer arithmetic, Kind 2 performs a fast approximate quantifier elimination. Otherwise, the quantifier elimination is delegated to an SMT solver, which is at this time only possible with Z3 or cvc5.

Options

--qe_method {precise|impl|cooper} (default cooper) – select the quantifier elimination strategy: cooper (default) 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 an conjunctive implicant first. If the problem is not in linear integer arithmetic, cooper falls back to impl.

--ic3_check_inductive <bool> (default true) – Check if a blocking clause is inductive and communicate it as an invariant to concurrent verification engines.

--ic3_block_in_future  <bool> (default true) – Block each clause not only in the frame it was discovered, but also in all higher frames.

--ic3_fwd_prop_non_gen <bool> (default true) – Attempt forward propagation of clauses before inductive generalization.

--ic3_fwd_prop_ind_gen <bool> (default true) – Inductively generalize clauses after forward propagation.

--ic3_fwd_prop_subsume <bool> (default true) – Check syntactic subsumption of forward propagated clauses