Full description
Kind 2 is an open-source, multi-engine, SMT-based automatic model checker
for safety properties of finite-state or infinite-state synchronous
reactive systems expressed as in an extension of the Lustre language. In
its basic configuration it takes as input one or more Lustre files
annotated with properties to be proven invariant, and outputs for each
property either a confirmation or a counterexample, i.e., a sequence inputs
that falsifies the property. More advanced features include contract-based
compositional verification, proof generation for proven properties, and
contract-based test generation.
Packages