You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
# This file is generated by dune, edit dune-project instead
2
+
opam-version: "2.0"
3
+
synopsis:
4
+
"Multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs"
5
+
description: """
6
+
Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of finite-state
7
+
or infinite-state synchronous reactive systems expressed as in an extension of the Lustre language.
8
+
In its basic configuration it takes as input a Lustre file annotated with properties to be proven invariant,
9
+
and outputs for each property either a confirmation or a counterexample, i.e., a sequence inputs that falsifies the property.
10
+
More advanced features include contract-based compositional verification, proof generation for proven properties, and contract-based test generation."""
0 commit comments