kind2version

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.

AuthorThe Kind 2 development team
LicenseApache-2.0
Published
Homepagehttps://kind2-mc.github.io/kind2
Issue Trackerhttps://github.com/kind2-mc/kind2/issues
MaintainerDaniel Larraz <daniel-larraz@uiowa.edu>
Dependencies
Source [http] https://github.com/kind2-mc/kind2/archive/v1.3.0.tar.gz
md5=3db351557e5acc9b05c98d5ec6492ebe
sha512=a66257bb6aa006260c9bc6d842058b1f882962e94d819b11d04cea9d8f86559a4013af21284350bd35df4c6f3355d85f93525f3f414582eb9d944c6b168701b8
StatisticsInstalled 2 times last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/kind2/kind2.1.3.0/opam
No package is dependent