kind2

Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs
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 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.

Install
Published
19 May 2022
Sources
v1.6.0.tar.gz
md5=b4257cab9be24044a4c883cadaa29a5b
sha512=7bf688042c823f485bbed807529bbcc4fc6cfd2f48011ecba62dfecf2d96328c34cb34a632ec027babeb1999a6936ba57dbd45e5a2a0f0882bcf1ffb8a1266e6
Dependencies
zmq
>= "5.1.0"
ounit2
with-test
odoc
with-doc
menhir
>= "20180523"
dune
>= "2.7"
ocaml
>= "4.09"
Reverse Dependencies