package kind2

All checked builds pass
  1. Overview
  2. Docs
Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs

Install 

dune-project
 Dependency

kind2-mc.github.io Changelog Edit opam file Versions (15)

Authors

  1. T
    The Kind 2 development team

Maintainers

  1. D
    Daniel Larraz <daniel-larraz@uiowa.edu>

Sources

v2.3.0.tar.gz
md5=5b5edead12973bbde03b7f3481bf6713
sha512=74593684a98f65b0832fe13b285010a5002479f77455ef1c4c3e80112ba4e0b7e2d51fa929430c47a262b56799961f3164ad93a469c7c4c6436a46908522dad9

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.

Added to opam-repository:

Dependencies (7)

  1. zmq >= "5.1.0"
  2. yojson < "3"
  3. num
  4. menhir >= "20180523" & < "20260112"
  5. dune-build-info
  6. dune >= "2.7"
  7. ocaml >= "4.09"

Dev Dependencies (2)

  1. ounit2 with-test
  2. odoc with-doc

Optional Dependencies

None

Used by

None

Conflicts

None

Build status

Results of building kind2 with each compiler on check.ci.ocaml.org, run of against opam-repository 7cdc698. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
3.0.0 n/a n/a good good good
2.3.0 (this version) good good good good good
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure