Kind 2 v1.5.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Print a deadlocking trace and a set of conflicting constraints when a contract is proven unrealizable.
• Multiple nodes can be annotated as main nodes so that analysis results for common subnodes are shared in modular analysis.
• New option to dump each counterexample to a file (--dump_cex).

Thanks to M. Anthony Aiello, Andreas Katis, and Amos Robinson for their feedback and suggestions.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

N.B. To run the Ubuntu and macOS binaries the ZeroMQ library (version 4.x or later) must be installed on your computer. You can install it by running sudo apt-get install libzmq5 in Ubuntu, or brew install zmq in macOS.

Kind 2 v1.4.0

This version includes performance improvements, bug fixes, some changes in the analysis behaviour, and a new feature for checking contracts of imported nodes.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

To run the Ubuntu and macOS binaries, the ZeroMQ library (version 4.x or later) must be installed on your computer. You can install it by running sudo apt-get install libzmq5 in Ubuntu, or brew install zmq in macOS.

Kind 2 v1.3.1

This release includes performance improvements and various fixes. Notably:

• Fix soundness issue in path compression when there are temporal dependencies
  between input values. (Thank you to M. Anthony Aiello for finding this bug).
• Fix bug in extraction of an active path during IC3 generalization.
• Improve IC3 performance over large models that contain reals or machine integers.
• Fix issue reading models from the latest version of Z3 (4.8.10).
  It caused a runtime error during IVC generation.

Kind 2 v1.3.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Computation of Inductive Validity Cores and Minimal Cut Sets.
• Invariant generation for machine integers.
• IC3 model checking engine for machine integers.
• Support for abstract types (thanks to Amos Robinson).
• Support for SMT solvers Boolector and MathSAT.
• A new command-line option to only parse Lustre inputs.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

N.B. To run the Ubuntu and macOS binaries the ZeroMQ library (version 4.x or later) must be installed on your computer. You can install it by running sudo apt-get install libzmq5 in Ubuntu, or brew install zmq in macOS.

Kind 2 v1.2.0

New features:

• Support for machine integers.
• Option to output results in JSON format.
• Interpreter accepts input values in JSON format.

Many bug fixes!

Please refer to the user documentation for more details.

Kind 2 v1.1.0

In addition to several internal changes, many improvements and some bug fixes, this release includes the following new functionalities:

• docker integration, see Kind 2's docker page
• support for Scade 6 automata and arrays
• arithmetic (integer and real) invariant generation
• logging of strengthening invariants on safe systems (experimental)

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

Kind 2 v1.0.1

Changes from 1.0.0: read Lustre from standard input

---

This version adds features that improve performance as well as provide new functionality. Notably these include:

• A new assume/guarantee-based contract language
• Modular and compositional verification
• An improved graph based invariant generation technique
• Compilation of Lustre to Rust
• Test-case generation
• Proof certificate generation
• Many performance improvements and bug fixes

Please refer to the CHANGES for a more detailed description and to the documentation of these new features.

Kind 2 v1.0.0

This version adds features that improve performance as well as provide new functionality. Notably these include:

• A new assume/guarantee-based contract language
• Modular and compositional verification
• An improved graph based invariant generation technique
• Compilation of Lustre to Rust
• Test-case generation
• Proof certificate generation
• Many performance improvements and bug fixes

Please refer to the CHANGES for a more detailed description and to the documentation of these new features.

v1.0.alpha1

Merge pull request #367 from mebsout/develop

Improvements in parsing and flags

Kind 2 v0.8.0

Kind 2 v0.8.0 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of Lustre programs.

This version adds features that improve performance as well as provide new functionality. See CHANGES and the manual for more details. This release is an intermediate release, and the next release will include strategies for contract-based compositional verification, support for arrays, and other features currently under development.