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
20 May 2021
Sources
v1.4.0.tar.gz
md5=3e9281a5da3215b89ed9e492a6decc2a
sha512=65cd68ca00704421cc9def3b83df84bfa6854b4d5670e6c79d47b24c9d44bb309f7dfb37c0b5a210ae7a34d2552e9d2fa63e22c2a8b8ea27d592106b3ca29620
Dependencies
zmq
>= "5.1.0" & < "5.1.4"
z3
< "4.8.9" & with-test
ounit2
with-test
odoc
with-doc
menhir
< "20211215"
dune
>= "2.0"
ocaml
>= "4.07"
Reverse Dependencies