Package kind2.v1.3.1

[daniel-larraz]

kind2.v1.3.1

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.

---

• Homepage: https://kind2-mc.github.io/kind2
• Source repo: git+https://github.com/kind2-mc/kind2.git
• Bug tracker: https://github.com/kind2-mc/kind2/issues

---

🐫 Pull-request generated by opam-publish v2.0.3

[camelus]

Commit: 31830f4

@daniel-larraz has posted 2 contributions.

☀️ All lint checks passed 31830f4

• These packages passed lint tests: kind2.1.3.1

---

☀️ Installability check (+1)

• new installable packages (1): kind2.1.3.1

[kit-ty-kate]

Thanks! Could you return the fix in the opam file upstream? Using < instead of <= allows this package to take eventual future revisions of the z3.4.8.8 package

[daniel-larraz]

Could you return the fix in the opam file upstream? Using < instead of <= allows this package to take eventual future revisions of the z3.4.8.8 package

Sure. Thanks.