+49
packages/kind2/kind2.v1.7.0/opam
+49
packages/kind2/kind2.v1.7.0/opam
···+"Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs"+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 a Lustre file 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."""+"sha512=5f3b4f0a517b5cbdd194f4b7c968249a579170f3429c47a3f179ae36a7e2b0d01cffbc8670e190b7050081c43b119efa291fdcf04725ba3d4f9a86d5a9add3f6"