The invariant generation technique currently implemented in Kind 2 is an improved version of the one implemented in PKind. It works by instantiating templates on a set of terms provided by a syntactic analysis of the system.
The main improvement is that in Kind 2, invariant generation is modular. That is to say it can attempt to discover invariants for subnodes of the top node. The idea is that looking at small components and discovering invariants for them provides results faster than analyzing the system monolithically. To disable the modular behavior of invariant generation, use the option
There are two invariant generation techniques: one state (OS) and two state (TS). The former will only look for invariants between the state variables in the current state, while the latter tries to relate the current state with the previous state. The two are separated because as the system grows in size, two state invariant generation can become very expensive.
The one state and two state variants can be activated with
--enable INVGENOS and
--enable INVGEN respectively.
Note that, in theory, two state invariant generation is strictly more powerful than the one state version, albeit slower, since two state can also discover one state invariants. When both variants are running, Kind 2 optimizes two state invariant generation by forcing it to look only for two state invariants.
The bottom line is that running i) only two state invariant generation or ii) one state and two states will discover the same invariants. In the case of i) the same techniques seeks both one state and two state invariants at the same time, which is slower than ii) where one state and two state invariants are sought by different processes running in parallel.
Invariant generation can be tweaked using the following options. Note that this will affect both the one state and two state process if both are running.
--invgen_prune_trivial <bool> (default
true) – when invariants are discovered, do not communicate the ones that are direct consequences of the transition relation.
--invgen_max_succ <int> (default
1) – the number of unrolling to perform on subsystems before moving on to the next one in the hierarchy.
--invgen_lift_candidates <bool> (default
false) – if true, then candidate terms generated for subsystems will be lifted to their callers. Warning this might choke invariant generation with a huge number of candidates for large enough systems.
--invgen_mine_trans <bool> (default
false) – if true, the transition relation will be mined for candidate terms. Can make the set of candidate terms untractable.
--invgen_renice <int> (only positive values) – the bigger the parameter, the lower the priority of invariant generation will be for the operating system.
Lock Step K-induction¶
Another improvement on the PKind invariant generation is the way the search for a k-induction proof of the candidate invariants is performed. In PKind, a bounded model checking engine is run up to a certain depth
d and discovers falsifiable candidate invariants. The graph used to produce the potential invariants is refined based on this information. Once the bound on the depth is reached, an inductive step instance looks for actual invariants by unrolling up to
In Kind 2, base and step are performed in lock step. Once the candidate invariant graph has been updated by base for some depth, step runs at the same depth and broadcasts the invariants it discovers to the whole framework. It is thus possible to generate invariants earlier and thus speed up the whole analysis.