Summary
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 one or more Lustre files 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.
Versions
v1.9.0 :: 0/1.9.0 :: gentoo
- Modified
- License
- Apache-2.0
- Keywords
- ~amd64
- USE flags
- ocamlopt test
USE flags
General
Dependencies
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
dev-ml / dune : A composable build system for OCaml
dev-ml / menhir : LR(1) parser generator for the OCaml language
dev-ml / num : Library for arbitrary-precision integer and rational arithmetic
dev-ml / yojson : JSON parsing and pretty-printing library for OCaml
Runtime Dependencies
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
dev-ml / dune : A composable build system for OCaml
dev-ml / menhir : LR(1) parser generator for the OCaml language
dev-ml / num : Library for arbitrary-precision integer and rational arithmetic
dev-ml / yojson : JSON parsing and pretty-printing library for OCaml
Bugs
- 909732
- sci-mathematics/kind2-1.9.0 - ERROR: sci-mathematics/kind2-1.9.0::gentoo failed (compile phase):
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/kind2: new package; add 1.9.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>