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 (--compositional 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.
A recursive function
is refined the same way, in steps. In a compositional analysis its contract
stands in for its recursive calls; once its own analysis has proved that
contract, refining a call to it from another node or function first unrolls
the body of the function once, with its recursive calls abstracted by the
contract, then up to --rec_unrollings times (2 by default); the values
of the calls that a spurious counterexample relied on are given to the
refinements as well, so that they need not unroll the function as deep as
the calls go. The analysis
of the function itself, or of a function of its recursive group, is not
refined this way: there the contract remains the induction hypothesis of the
recursion.
Modifiers to control node/function abstraction
To prevent Kind 2 from abstracting a specific node or function that has both a body
and a contract during compositional analysis,
use the transparent modifier before the node or function keywords:
transparent function F(...) returns (...)To prevent Kind 2 from refining a specific node or function that has both a body
and a contract during compositional and modular analyses,
use the opaque modifier before the node or function keywords:
opaque node N(...) returns (...)