kind2
Multi-engine SMT-based automatic model checker
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.
homepage ↗homepage ↗ github: kind2-mc/kind2
Available in
| Overlay | Newest | Ebuilds | Last activity | |
|---|---|---|---|---|
| gentoo gitweb ↗ | 1.9.0 | 1 | 13 h | details › |
Versions & arches
Use flags of 1.9.0
- +ocamlopt Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
- test Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)