k-Induction is a well-known technique for the verification of transition systems. A k-induction engine is composed of two parts: base and step. Base performs bounded model checking on the properties, i.e. checks the base case. Step checks whether it is possible to reach a violation of one of the properties from a trace of states satisfying them: the inductive step.
In Kind 2 base and step run in parallel, and can be enabled separately. Running step alone with
kind2 --enable IND <file>
will not yield anything interesting, as step cannot falsify properties nor prove anything without base. To run the actual k-induction engine, you must enable base (
BMC) and step (
kind2 --enable BMC --enable IND <file>
k-Induction can be tweaked with the following options.
--bmc_max <int> (default
0) – sets an upper bound on the number of unrolling base and step will perform.
0 is for unlimited.
--ind_compress <bool> (default
false) – activates path compression in step, i.e. counterexamples with a loop will be dismissed. You can activate several path compression strategies:
true) – compresses states if they are equal modulo inputs
false) – compresses states if they have the same successors (experimental)
false) – compresses states if they have the same predecessors (experimental)
--ind_lazy_invariants <bool> (default
false) – deactivates eager use of invariants in step. Instead, when a step counterexample is found each invariant is evaluated on the model until one blocks it. The invariant is then asserted to block the counterexample, and step starts a new check-sat.