Techniques¶

This section presents the techniques available in Kind 2: how they work, and how they can be tweaked through various options:

Compositional reasoning¶

When verifying a node `n`, compositional reasoning consists in abstracting the complexity of the subnodes of `n` by their contracts (see Contract Semantics). The idea is that the contract has typically a lot less state than the node it specifies, which in addition to its own state contains that of its subnodes recursively.

Compositional reasoning thus improves the scalability of Kind 2 by taking advantage of information provided by the user to abstract the complexity away. When in compositional mode (`--composition true`), Kind 2 will abstract all calls (to subnodes that have a contract with at least one guarantee or one mode) in the top node and verify the resulting, abstract system.

A successful compositional proof of a node does not guarantee the correctness of the concrete (un-abstracted) node though, since the subnodes have not been verified. For this reason compositional reasoning is usually applied in conjunction with modular reasoning, discussed in the next section.

Modular reasoning¶

Modular reasoning is activated with the option `--modular true`. In this mode, Kind 2 will perform whatever type of analysis is specified by the other flags on every node of the hierarchy, bottom-up. The analysis is completed on every node even if some node is proved unsafe because of the falsification of one of its properties.

A timeout for each analysis can be specified using the `--timeout_analysis` flag. It can be used in conjunction with the global timeout given with the `--timeout` or `--timeout_wall` time.

Internally Kind 2 builds on previous analyses when starting a new one. For instance, by using the invariants previously discovered in subnodes of the node under analysis.

Refinement in compositional and modular analyses¶

An interesting configuration is

```kind2 --modular true --compositional true ...
```

If `top` calls `sub` and we analyze `top`, it means we have previously analyzed `sub`. We are running in compositional mode so the call to `sub` is originally abstracted by its contract. Say the analysis fails with a counterexample. The counterexample might be spurious for the concrete version of `sub`: the failure would not happen if we used the concrete call to `sub` instead of the abstract one.

Say now that when we analyzed `sub`, we proved that it is correct. In this case Kind 2 will attempt to refine the call to `sub` in top. That is, undo the abstraction and use the implementation of `sub` in a new analysis.

Note that since `sub` is known to be correct, it is stronger than its contract. More precisely, it accepts fewer execution traces than its contract does. Hence anything proved with the abstraction of `sub` is still valid after refinement, and Kind 2 will use these results right away.